albertqjiang / int Goto Github PK

Traceback (most recent call last):
  File "/home/jychen/.conda/envs/jychen_main/lib/python3.10/site-packages/IPython/core/interactiveshell.py", line 3433, in run_code
    exec(code_obj, self.user_global_ns, self.user_ns)
  File "/tmp/ipykernel_21573/176925322.py", line 1, in <module>
    evaluate.interact_with_prover_sequentially(
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/evaluate.py", line 186, in interact_with_prover_sequentially
    print('obs_after_action', prover.get_observation_string())
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/wrapped_prover.py", line 25, in get_observation_string
    return self.inner.parser.observation_to_source(self.inner.get_observation())
  File "/data/jychen/research/code/third_party/INT/int_environment/proof_system/graph_seq_conversion.py", line 101, in observation_to_source
    source = source + logic_statement_to_seq_string(observation["objectives"][0])
IndexError: list index out of range

File /data/jychen/research/code/research_mono/neural_theorem_prover/evaluate.py:182, in _interact_with_prover_sequentially_single(initial_step, max_steps, debug_name, verbose)
    180 for action in actions:
    181     lemma, input_entities = prover.find_action(action)
--> 182     result = prover.inner.apply_theorem(lemma, input_entities)
    183     result_info = prover.interpret_result(result)
    185     if verbose:

File /data/jychen/research/code/third_party/INT/int_environment/proof_system/prover.py:169, in Prover.apply_theorem(self, theorem, operands)
    167 def apply_theorem(self, theorem, operands):
    168     # Apply a theorem with operands
--> 169     results = theorem.execute_th(operands, mode=self.mode_theorem)
    170     assumptions, conclusions = results["Assumptions"], results["Conclusions"]
    172     # Prevent the scenario [0, 1] -> [0]

File /data/jychen/research/code/third_party/INT/int_environment/proof_system/field_axioms.py:1364, in EquMoveTerm.execute_th(self, operands, mode)
   1359 elif mode == "prove":
   1360     """
   1361     a + b = c, ls(a) => ls(c + (-b))
   1362     2 inputs: [a, c + (-b)]
   1363     """
-> 1364     a, c_minus_b, = [deepcopy(op) for op in operands]
   1365     if is_entity(a) and is_entity(c_minus_b) and is_structured(c_minus_b, "add") \
   1366             and is_structured(c_minus_b.operands[1], "opp"):
   1367         c, minus_b, = c_minus_b.operands

ValueError: not enough values to unpack (expected 2, got 1)