%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SWX071+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Apr 1 02:15:23 AM UTC 2025
% Result : Unknown 3.33s 3.64s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWX071+1 : TPTP v9.1.0. Released v9.1.0.
% 0.03/0.11 % Command : otter-tptp-script %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Mon Mar 31 15:54:31 EDT 2025
% 0.11/0.31 % CPUTime :
% 3.33/3.62 ----- Otter 3.3f, August 2004 -----
% 3.33/3.62 The process was started by sandbox2 on n032.cluster.edu,
% 3.33/3.62 Mon Mar 31 15:54:31 2025
% 3.33/3.62 The command was "./otter". The process ID is 23903.
% 3.33/3.62
% 3.33/3.62 set(prolog_style_variables).
% 3.33/3.62 set(auto).
% 3.33/3.62 dependent: set(auto1).
% 3.33/3.62 dependent: set(process_input).
% 3.33/3.62 dependent: clear(print_kept).
% 3.33/3.62 dependent: clear(print_new_demod).
% 3.33/3.62 dependent: clear(print_back_demod).
% 3.33/3.62 dependent: clear(print_back_sub).
% 3.33/3.62 dependent: set(control_memory).
% 3.33/3.62 dependent: assign(max_mem, 12000).
% 3.33/3.62 dependent: assign(pick_given_ratio, 4).
% 3.33/3.62 dependent: assign(stats_level, 1).
% 3.33/3.62 dependent: assign(max_seconds, 10800).
% 3.33/3.62 clear(print_given).
% 3.33/3.62
% 3.33/3.62 formula_list(usable).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 - ( =(nil, ***HERE*** '1') ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 - ( =(nil, ***HERE*** '0') ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx20 Xx21 ( - ( =( ***HERE*** '1',cons(Xx20,Xx21)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx22 Xx23 ( - ( =( ***HERE*** '0',cons(Xx22,Xx23)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 - ( =( ***HERE*** '1','0') ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx38 ( - ( =( ***HERE*** '1',p(Xx38)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx39 ( - ( =( ***HERE*** '1',neg(Xx39)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx40 Xx41 ( - ( =( ***HERE*** '1',and(Xx40,Xx41)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx42 Xx43 ( - ( =( ***HERE*** '1',or(Xx42,Xx43)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx44 ( - ( =( ***HERE*** '0',p(Xx44)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx45 ( - ( =( ***HERE*** '0',neg(Xx45)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx46 Xx47 ( - ( =( ***HERE*** '0',and(Xx46,Xx47)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 0
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 ( all Xx48 Xx49 ( - ( =( ***HERE*** '0',or(Xx48,Xx49)) ) ) ).
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.62 '
% 3.33/3.62 1
% 3.33/3.62 '
% 3.33/3.62
% 3.33/3.62 The context of the bad sequence is:
% 3.33/3.62
% 3.33/3.62
% 3.33/3.62 gr( ***HERE*** '1').
% 3.33/3.62
% 3.33/3.62 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.62 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 gr( ***HERE*** '0').
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xx1 Xx2 Xx3 (
% 3.33/3.64 ( eval_succeeds(Xx1,Xx2,Xx3)
% 3.33/3.64 <-> ( ( exists Xx4 Xx5 (
% 3.33/3.64 ( =(Xx1,or(Xx4,Xx5))
% 3.33/3.64 & =(Xx3, ***HERE*** '0')
% 3.33/3.64 & eval_succeeds(Xx4,Xx2,'0')
% 3.33/3.64 & eval_succeeds(Xx5,Xx2,'0') ) ) )
% 3.33/3.64 | ( exists Xx6 Xx7 (
% 3.33/3.64 ( =(Xx1,or(Xx6,Xx7))
% 3.33/3.64 & =(Xx3,'1')
% 3.33/3.64 & eval_succeeds(Xx7,Xx2,'1') ) ) )
% 3.33/3.64 | ( exists Xx8 Xx9 (
% 3.33/3.64 ( =(Xx1,or(Xx8,Xx9))
% 3.33/3.64 & =(Xx3,'1')
% 3.33/3.64 & eval_succeeds(Xx8,Xx2,'1') ) ) )
% 3.33/3.64 | ( exists Xx10 Xx11 (
% 3.33/3.64 ( =(Xx1,and(Xx10,Xx11))
% 3.33/3.64 & =(Xx3,'0')
% 3.33/3.64 & eval_succeeds(Xx11,Xx2,'0') ) ) )
% 3.33/3.64 | ( exists Xx12 Xx13 (
% 3.33/3.64 ( =(Xx1,and(Xx12,Xx13))
% 3.33/3.64 & =(Xx3,'0')
% 3.33/3.64 & eval_succeeds(Xx12,Xx2,'0') ) ) )
% 3.33/3.64 | ( exists Xx14 Xx15 (
% 3.33/3.64 ( =(Xx1,and(Xx14,Xx15))
% 3.33/3.64 & =(Xx3,'1')
% 3.33/3.64 & eval_succeeds(Xx14,Xx2,'1')
% 3.33/3.64 & eval_succeeds(Xx15,Xx2,'1') ) ) )
% 3.33/3.64 | ( exists Xx16 (
% 3.33/3.64 ( =(Xx1,neg(Xx16))
% 3.33/3.64 & =(Xx3,'0')
% 3.33/3.64 & eval_succeeds(Xx16,Xx2,'1') ) ) )
% 3.33/3.64 | ( exists Xx17 (
% 3.33/3.64 ( =(Xx1,neg(Xx17))
% 3.33/3.64 & =(Xx3,'1')
% 3.33/3.64 & eval_succeeds(Xx17,Xx2,'0') ) ) )
% 3.33/3.64 | ( exists Xx18 (
% 3.33/3.64 ( =(Xx1,p(Xx18))
% 3.33/3.64 & =(Xx3,'0')
% 3.33/3.64 & member_succeeds(neg(p(Xx18)),Xx2) ) ) )
% 3.33/3.64 | ( exists Xx19 (
% 3.33/3.64 ( =(Xx1,p(Xx19))
% 3.33/3.64 & =(Xx3,'1')
% 3.33/3.64 & member_succeeds(p(Xx19),Xx2) ) ) ) ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xx1 Xx2 Xx3 (
% 3.33/3.64 ( eval_fails(Xx1,Xx2,Xx3)
% 3.33/3.64 <-> ( ( all Xx4 Xx5 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx4,Xx5)) )
% 3.33/3.64 | - ( =(Xx3, ***HERE*** '0') )
% 3.33/3.64 | eval_fails(Xx4,Xx2,'0')
% 3.33/3.64 | eval_fails(Xx5,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx6 Xx7 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx6,Xx7)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_fails(Xx7,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx8 Xx9 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx8,Xx9)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_fails(Xx8,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx10 Xx11 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx10,Xx11)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_fails(Xx11,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx12 Xx13 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx12,Xx13)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_fails(Xx12,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx14 Xx15 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx14,Xx15)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_fails(Xx14,Xx2,'1')
% 3.33/3.64 | eval_fails(Xx15,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx16 (
% 3.33/3.64 ( - ( =(Xx1,neg(Xx16)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_fails(Xx16,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx17 (
% 3.33/3.64 ( - ( =(Xx1,neg(Xx17)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_fails(Xx17,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx18 (
% 3.33/3.64 ( - ( =(Xx1,p(Xx18)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | member_fails(neg(p(Xx18)),Xx2) ) ) )
% 3.33/3.64 & ( all Xx19 (
% 3.33/3.64 ( - ( =(Xx1,p(Xx19)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | member_fails(p(Xx19),Xx2) ) ) ) ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xx1 Xx2 Xx3 (
% 3.33/3.64 ( eval_terminates(Xx1,Xx2,Xx3)
% 3.33/3.64 <-> ( ( all Xx4 Xx5 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx4,Xx5)) )
% 3.33/3.64 | - ( =(Xx3, ***HERE*** '0') )
% 3.33/3.64 | ( eval_terminates(Xx4,Xx2,'0')
% 3.33/3.64 & ( eval_fails(Xx4,Xx2,'0')
% 3.33/3.64 | eval_terminates(Xx5,Xx2,'0') ) ) ) ) )
% 3.33/3.64 & ( all Xx6 Xx7 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx6,Xx7)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_terminates(Xx7,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx8 Xx9 (
% 3.33/3.64 ( - ( =(Xx1,or(Xx8,Xx9)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_terminates(Xx8,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx10 Xx11 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx10,Xx11)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_terminates(Xx11,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx12 Xx13 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx12,Xx13)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_terminates(Xx12,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx14 Xx15 (
% 3.33/3.64 ( - ( =(Xx1,and(Xx14,Xx15)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | ( eval_terminates(Xx14,Xx2,'1')
% 3.33/3.64 & ( eval_fails(Xx14,Xx2,'1')
% 3.33/3.64 | eval_terminates(Xx15,Xx2,'1') ) ) ) ) )
% 3.33/3.64 & ( all Xx16 (
% 3.33/3.64 ( - ( =(Xx1,neg(Xx16)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | eval_terminates(Xx16,Xx2,'1') ) ) )
% 3.33/3.64 & ( all Xx17 (
% 3.33/3.64 ( - ( =(Xx1,neg(Xx17)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | eval_terminates(Xx17,Xx2,'0') ) ) )
% 3.33/3.64 & ( all Xx18 (
% 3.33/3.64 ( - ( =(Xx1,p(Xx18)) )
% 3.33/3.64 | - ( =(Xx3,'0') )
% 3.33/3.64 | member_terminates(neg(p(Xx18)),Xx2) ) ) )
% 3.33/3.64 & ( all Xx19 (
% 3.33/3.64 ( - ( =(Xx1,p(Xx19)) )
% 3.33/3.64 | - ( =(Xx3,'1') )
% 3.33/3.64 | member_terminates(p(Xx19),Xx2) ) ) ) ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 1
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xa Xi Xj (
% 3.33/3.64 ( true_succeeds(Xa,Xi,Xj)
% 3.33/3.64 -> eval_succeeds(Xa,Xj, ***HERE*** '1') ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xa Xi Xj (
% 3.33/3.64 ( false_succeeds(Xa,Xi,Xj)
% 3.33/3.64 -> eval_succeeds(Xa,Xj, ***HERE*** '0') ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 1
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xa Xi (
% 3.33/3.64 ( defined_succeeds(Xa,Xi)
% 3.33/3.64 -> ( eval_succeeds(Xa,Xi, ***HERE*** '1')
% 3.33/3.64 | eval_succeeds(Xa,Xi,'0') ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xa (
% 3.33/3.64 ( valid_fails(Xa)
% 3.33/3.64 -> ( exists Xi (
% 3.33/3.64 ( interpretation_succeeds(Xi)
% 3.33/3.64 & eval_succeeds(Xa,Xi, ***HERE*** '0') ) ) ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 0
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 ( all Xa Xh Xx (
% 3.33/3.64 ( ( ( exists Xx4 Xx5 (
% 3.33/3.64 ( =(Xa,or(Xx4,Xx5))
% 3.33/3.64 & =(Xx, ***HERE*** '0')
% 3.33/3.64 & eval_succeeds(Xx4,Xh,'0')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('0','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx4,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('0','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx4,Xi,Xj) ) ) ) ) ) ) ) ) )
% 3.33/3.64 & eval_succeeds(Xx5,Xh,'0')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('0','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx5,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('0','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx5,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx6 Xx7 (
% 3.33/3.64 ( =(Xa,or(Xx6,Xx7))
% 3.33/3.64 & =(Xx,'1')
% 3.33/3.64 & eval_succeeds(Xx7,Xh,'1')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('1','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx7,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('1','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx7,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx8 Xx9 (
% 3.33/3.64 ( =(Xa,or(Xx8,Xx9))
% 3.33/3.64 & =(Xx,'1')
% 3.33/3.64 & eval_succeeds(Xx8,Xh,'1')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('1','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx8,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('1','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx8,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx10 Xx11 (
% 3.33/3.64 ( =(Xa,and(Xx10,Xx11))
% 3.33/3.64 & =(Xx,'0')
% 3.33/3.64 & eval_succeeds(Xx11,Xh,'0')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('0','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx11,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('0','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx11,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx12 Xx13 (
% 3.33/3.64 ( =(Xa,and(Xx12,Xx13))
% 3.33/3.64 & =(Xx,'0')
% 3.33/3.64 & eval_succeeds(Xx12,Xh,'0')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('0','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx12,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('0','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx12,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx14 Xx15 (
% 3.33/3.64 ( =(Xa,and(Xx14,Xx15))
% 3.33/3.64 & =(Xx,'1')
% 3.33/3.64 & eval_succeeds(Xx14,Xh,'1')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('1','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx14,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('1','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx14,Xi,Xj) ) ) ) ) ) ) ) ) )
% 3.33/3.64 & eval_succeeds(Xx15,Xh,'1')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('1','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx15,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('1','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx15,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx16 (
% 3.33/3.64 ( =(Xa,neg(Xx16))
% 3.33/3.64 & =(Xx,'0')
% 3.33/3.64 & eval_succeeds(Xx16,Xh,'1')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('1','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx16,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('1','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx16,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx17 (
% 3.33/3.64 ( =(Xa,neg(Xx17))
% 3.33/3.64 & =(Xx,'1')
% 3.33/3.64 & eval_succeeds(Xx17,Xh,'0')
% 3.33/3.64 & ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =('0','1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xx17,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =('0','0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xx17,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 | ( exists Xx18 (
% 3.33/3.64 ( =(Xa,p(Xx18))
% 3.33/3.64 & =(Xx,'0')
% 3.33/3.64 & member_succeeds(neg(p(Xx18)),Xh) ) ) )
% 3.33/3.64 | ( exists Xx19 (
% 3.33/3.64 ( =(Xa,p(Xx19))
% 3.33/3.64 & =(Xx,'1')
% 3.33/3.64 & member_succeeds(p(Xx19),Xh) ) ) ) )
% 3.33/3.64 -> ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =(Xx,'1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xa,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =(Xx,'0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xa,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) )
% 3.33/3.64 -> ( all Xa Xh Xx (
% 3.33/3.64 ( eval_succeeds(Xa,Xh,Xx)
% 3.33/3.64 -> ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =(Xx,'1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xa,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =(Xx,'0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xa,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) ).
% 3.33/3.64
% 3.33/3.64 ERROR, the 3 terms/operators in the following sequence are OK, but they
% 3.33/3.64 could not be combined into a single term with special operators.
% 3.33/3.64 '
% 3.33/3.64 1
% 3.33/3.64 '
% 3.33/3.64
% 3.33/3.64 The context of the bad sequence is:
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64
% 3.33/3.64 - ( ( all Xa Xh Xx (
% 3.33/3.64 ( eval_succeeds(Xa,Xh,Xx)
% 3.33/3.64 -> ( interpretation_succeeds(Xh)
% 3.33/3.64 -> ( all Xi (
% 3.33/3.64 ( ( literal_list_succeeds(Xi)
% 3.33/3.64 & sub(Xi,Xh) )
% 3.33/3.64 -> ( ( =(Xx, ***HERE*** '1')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & true_succeeds(Xa,Xi,Xj) ) ) ) )
% 3.33/3.64 & ( =(Xx,'0')
% 3.33/3.64 -> ( exists Xj (
% 3.33/3.64 ( sub(Xj,Xh)
% 3.33/3.64 & false_succeeds(Xa,Xi,Xj) ) ) ) ) ) ) ) ) ) ) ) ) ).
% 3.33/3.64 all A (A=A).
% 3.33/3.64 all Xx4 Xx5 (nil!=cons(Xx4,Xx5)).
% 3.33/3.64 all Xx6 (nil!=p(Xx6)).
% 3.33/3.64 all Xx7 (nil!=neg(Xx7)).
% 3.33/3.64 all Xx8 Xx9 (nil!=and(Xx8,Xx9)).
% 3.33/3.64 all Xx10 Xx11 (nil!=or(Xx10,Xx11)).
% 3.33/3.64 all Xx12 Xx13 Xx14 Xx15 (cons(Xx12,Xx13)=cons(Xx14,Xx15)->Xx13=Xx15).
% 3.33/3.64 all Xx16 Xx17 Xx18 Xx19 (cons(Xx16,Xx17)=cons(Xx18,Xx19)->Xx16=Xx18).
% 3.33/3.64 all Xx24 Xx25 Xx26 (cons(Xx24,Xx25)!=p(Xx26)).
% 3.33/3.64 all Xx27 Xx28 Xx29 (cons(Xx27,Xx28)!=neg(Xx29)).
% 3.33/3.64 all Xx30 Xx31 Xx32 Xx33 (cons(Xx30,Xx31)!=and(Xx32,Xx33)).
% 3.33/3.64 all Xx34 Xx35 Xx36 Xx37 (cons(Xx34,Xx35)!=or(Xx36,Xx37)).
% 3.33/3.64 all Xx50 Xx51 (p(Xx50)=p(Xx51)->Xx50=Xx51).
% 3.33/3.64 all Xx52 Xx53 (p(Xx52)!=neg(Xx53)).
% 3.33/3.64 all Xx54 Xx55 Xx56 (p(Xx54)!=and(Xx55,Xx56)).
% 3.33/3.64 all Xx57 Xx58 Xx59 (p(Xx57)!=or(Xx58,Xx59)).
% 3.33/3.64 all Xx60 Xx61 (neg(Xx60)=neg(Xx61)->Xx60=Xx61).
% 3.33/3.64 all Xx62 Xx63 Xx64 (neg(Xx62)!=and(Xx63,Xx64)).
% 3.33/3.64 all Xx65 Xx66 Xx67 (neg(Xx65)!=or(Xx66,Xx67)).
% 3.33/3.64 all Xx68 Xx69 Xx70 Xx71 (and(Xx68,Xx69)=and(Xx70,Xx71)->Xx69=Xx71).
% 3.33/3.64 all Xx72 Xx73 Xx74 Xx75 (and(Xx72,Xx73)=and(Xx74,Xx75)->Xx72=Xx74).
% 3.33/3.64 all Xx76 Xx77 Xx78 Xx79 (and(Xx76,Xx77)!=or(Xx78,Xx79)).
% 3.33/3.64 all Xx80 Xx81 Xx82 Xx83 (or(Xx80,Xx81)=or(Xx82,Xx83)->Xx81=Xx83).
% 3.33/3.64 all Xx84 Xx85 Xx86 Xx87 (or(Xx84,Xx85)=or(Xx86,Xx87)->Xx84=Xx86).
% 3.33/3.64 gr(nil).
% 3.33/3.64 all Xx88 Xx89 (gr(Xx88)&gr(Xx89)<->gr(cons(Xx88,Xx89))).
% 3.33/3.64 all Xx90 (gr(Xx90)<->gr(p(Xx90))).
% 3.33/3.64 all Xx91 (gr(Xx91)<->gr(neg(Xx91))).
% 3.33/3.64 all Xx92 Xx93 (gr(Xx92)&gr(Xx93)<->gr(and(Xx92,Xx93))).
% 3.33/3.64 all Xx94 Xx95 (gr(Xx94)&gr(Xx95)<->gr(or(Xx94,Xx95))).
% 3.33/3.64 all Xx96 Xx97 (-(defined_succeeds(Xx96,Xx97)&defined_fails(Xx96,Xx97))).
% 3.33/3.64 all Xx96 Xx97 (defined_terminates(Xx96,Xx97)->defined_succeeds(Xx96,Xx97)|defined_fails(Xx96,Xx97)).
% 3.33/3.64 all Xx98 Xx99 Xx100 (-(eval_succeeds(Xx98,Xx99,Xx100)&eval_fails(Xx98,Xx99,Xx100))).
% 3.33/3.64 all Xx98 Xx99 Xx100 (eval_terminates(Xx98,Xx99,Xx100)->eval_succeeds(Xx98,Xx99,Xx100)|eval_fails(Xx98,Xx99,Xx100)).
% 3.33/3.64 all Xx101 Xx102 Xx103 (-(false_succeeds(Xx101,Xx102,Xx103)&false_fails(Xx101,Xx102,Xx103))).
% 3.33/3.64 all Xx101 Xx102 Xx103 (false_terminates(Xx101,Xx102,Xx103)->false_succeeds(Xx101,Xx102,Xx103)|false_fails(Xx101,Xx102,Xx103)).
% 3.33/3.64 all Xx104 Xx105 Xx106 (-(true_succeeds(Xx104,Xx105,Xx106)&true_fails(Xx104,Xx105,Xx106))).
% 3.33/3.64 all Xx104 Xx105 Xx106 (true_terminates(Xx104,Xx105,Xx106)->true_succeeds(Xx104,Xx105,Xx106)|true_fails(Xx104,Xx105,Xx106)).
% 3.33/3.64 all Xx107 (-(satisfiable_succeeds(Xx107)&satisfiable_fails(Xx107))).
% 3.33/3.64 all Xx107 (satisfiable_terminates(Xx107)->satisfiable_succeeds(Xx107)|satisfiable_fails(Xx107)).
% 3.33/3.64 all Xx108 (-(valid_succeeds(Xx108)&valid_fails(Xx108))).
% 3.33/3.64 all Xx108 (valid_terminates(Xx108)->valid_succeeds(Xx108)|valid_fails(Xx108)).
% 3.33/3.64 all Xx109 (-(incon_succeeds(Xx109)&incon_fails(Xx109))).
% 3.33/3.64 all Xx109 (incon_terminates(Xx109)->incon_succeeds(Xx109)|incon_fails(Xx109)).
% 3.33/3.64 all Xx110 (-(interpretation_succeeds(Xx110)&interpretation_fails(Xx110))).
% 3.33/3.64 all Xx110 (interpretation_terminates(Xx110)->interpretation_succeeds(Xx110)|interpretation_fails(Xx110)).
% 3.33/3.64 all Xx111 (-(literal_list_succeeds(Xx111)&literal_list_fails(Xx111))).
% 3.33/3.64 all Xx111 (literal_list_terminates(Xx111)->literal_list_succeeds(Xx111)|literal_list_fails(Xx111)).
% 3.33/3.64 all Xx112 (-(literal_succeeds(Xx112)&literal_fails(Xx112))).
% 3.33/3.64 all Xx112 (literal_terminates(Xx112)->literal_succeeds(Xx112)|literal_fails(Xx112)).
% 3.33/3.64 all Xx113 (-(formula_succeeds(Xx113)&formula_fails(Xx113))).
% 3.33/3.64 all Xx113 (formula_terminates(Xx113)->formula_succeeds(Xx113)|formula_fails(Xx113)).
% 3.33/3.64 all Xx114 Xx115 (-(member_succeeds(Xx114,Xx115)&member_fails(Xx114,Xx115))).
% 3.33/3.64 all Xx114 Xx115 (member_terminates(Xx114,Xx115)->member_succeeds(Xx114,Xx115)|member_fails(Xx114,Xx115)).
% 3.33/3.64 all Xx116 (-(list_succeeds(Xx116)&list_fails(Xx116))).
% 3.33/3.64 all Xx116 (list_terminates(Xx116)->list_succeeds(Xx116)|list_fails(Xx116)).
% 3.33/3.64 all Xx1 Xx2 (defined_succeeds(Xx1,Xx2)<-> (exists Xx3 Xx4 (Xx1=or(Xx3,Xx4)&defined_succeeds(Xx3,Xx2)&defined_succeeds(Xx4,Xx2)))| (exists Xx5 Xx6 (Xx1=and(Xx5,Xx6)&defined_succeeds(Xx5,Xx2)&defined_succeeds(Xx6,Xx2)))| (exists Xx7 (Xx1=neg(Xx7)&defined_succeeds(Xx7,Xx2)))| (exists Xx8 (Xx1=p(Xx8)&member_succeeds(neg(p(Xx8)),Xx2)))| (exists Xx9 (Xx1=p(Xx9)&member_succeeds(p(Xx9),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 (defined_fails(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx1!=or(Xx3,Xx4)|defined_fails(Xx3,Xx2)|defined_fails(Xx4,Xx2)))& (all Xx5 Xx6 (Xx1!=and(Xx5,Xx6)|defined_fails(Xx5,Xx2)|defined_fails(Xx6,Xx2)))& (all Xx7 (Xx1!=neg(Xx7)|defined_fails(Xx7,Xx2)))& (all Xx8 (Xx1!=p(Xx8)|member_fails(neg(p(Xx8)),Xx2)))& (all Xx9 (Xx1!=p(Xx9)|member_fails(p(Xx9),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 (defined_terminates(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx1!=or(Xx3,Xx4)|defined_terminates(Xx3,Xx2)& (defined_fails(Xx3,Xx2)|defined_terminates(Xx4,Xx2))))& (all Xx5 Xx6 (Xx1!=and(Xx5,Xx6)|defined_terminates(Xx5,Xx2)& (defined_fails(Xx5,Xx2)|defined_terminates(Xx6,Xx2))))& (all Xx7 (Xx1!=neg(Xx7)|defined_terminates(Xx7,Xx2)))& (all Xx8 (Xx1!=p(Xx8)|member_terminates(neg(p(Xx8)),Xx2)))& (all Xx9 (Xx1!=p(Xx9)|member_terminates(p(Xx9),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (false_succeeds(Xx1,Xx2,Xx3)<-> (exists Xx4 Xx5 Xx6 (Xx1=or(Xx4,Xx5)&false_succeeds(Xx4,Xx2,Xx6)&false_succeeds(Xx5,Xx6,Xx3)))| (exists Xx7 Xx8 (Xx1=and(Xx7,Xx8)&false_succeeds(Xx8,Xx2,Xx3)))| (exists Xx9 Xx10 (Xx1=and(Xx9,Xx10)&false_succeeds(Xx9,Xx2,Xx3)))| (exists Xx11 (Xx1=neg(Xx11)&true_succeeds(Xx11,Xx2,Xx3)))| (exists Xx12 (Xx1=p(Xx12)&Xx3=cons(neg(p(Xx12)),Xx2)&member_fails(p(Xx12),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (false_fails(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 Xx6 (Xx1!=or(Xx4,Xx5)|false_fails(Xx4,Xx2,Xx6)|false_fails(Xx5,Xx6,Xx3)))& (all Xx7 Xx8 (Xx1!=and(Xx7,Xx8)|false_fails(Xx8,Xx2,Xx3)))& (all Xx9 Xx10 (Xx1!=and(Xx9,Xx10)|false_fails(Xx9,Xx2,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|true_fails(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(neg(p(Xx12)),Xx2)|member_succeeds(p(Xx12),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (false_terminates(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 Xx6 (Xx1!=or(Xx4,Xx5)|false_terminates(Xx4,Xx2,Xx6)& (false_fails(Xx4,Xx2,Xx6)|false_terminates(Xx5,Xx6,Xx3))))& (all Xx7 Xx8 (Xx1!=and(Xx7,Xx8)|false_terminates(Xx8,Xx2,Xx3)))& (all Xx9 Xx10 (Xx1!=and(Xx9,Xx10)|false_terminates(Xx9,Xx2,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|true_terminates(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(neg(p(Xx12)),Xx2)|member_terminates(p(Xx12),Xx2)&gr(p(Xx12))&gr(Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (true_succeeds(Xx1,Xx2,Xx3)<-> (exists Xx4 Xx5 (Xx1=or(Xx4,Xx5)&true_succeeds(Xx5,Xx2,Xx3)))| (exists Xx6 Xx7 (Xx1=or(Xx6,Xx7)&true_succeeds(Xx6,Xx2,Xx3)))| (exists Xx8 Xx9 Xx10 (Xx1=and(Xx8,Xx9)&true_succeeds(Xx8,Xx2,Xx10)&true_succeeds(Xx9,Xx10,Xx3)))| (exists Xx11 (Xx1=neg(Xx11)&false_succeeds(Xx11,Xx2,Xx3)))| (exists Xx12 (Xx1=p(Xx12)&Xx3=cons(p(Xx12),Xx2)&member_fails(neg(p(Xx12)),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (true_fails(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 (Xx1!=or(Xx4,Xx5)|true_fails(Xx5,Xx2,Xx3)))& (all Xx6 Xx7 (Xx1!=or(Xx6,Xx7)|true_fails(Xx6,Xx2,Xx3)))& (all Xx8 Xx9 Xx10 (Xx1!=and(Xx8,Xx9)|true_fails(Xx8,Xx2,Xx10)|true_fails(Xx9,Xx10,Xx3)))& (all Xx11 (Xx1!=neg(Xx11)|false_fails(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(p(Xx12),Xx2)|member_succeeds(neg(p(Xx12)),Xx2)))).
% 3.33/3.64 all Xx1 Xx2 Xx3 (true_terminates(Xx1,Xx2,Xx3)<-> (all Xx4 Xx5 (Xx1!=or(Xx4,Xx5)|true_terminates(Xx5,Xx2,Xx3)))& (all Xx6 Xx7 (Xx1!=or(Xx6,Xx7)|true_terminates(Xx6,Xx2,Xx3)))& (all Xx8 Xx9 Xx10 (Xx1!=and(Xx8,Xx9)|true_terminates(Xx8,Xx2,Xx10)& (true_fails(Xx8,Xx2,Xx10)|true_terminates(Xx9,Xx10,Xx3))))& (all Xx11 (Xx1!=neg(Xx11)|false_terminates(Xx11,Xx2,Xx3)))& (all Xx12 (Xx1!=p(Xx12)|Xx3!=cons(p(Xx12),Xx2)|member_terminates(neg(p(Xx12)),Xx2)&gr(neg(p(Xx12)))&gr(Xx2)))).
% 3.33/3.64 all Xx1 (satisfiable_succeeds(Xx1)<-> (exists Xx2 true_succeeds(Xx1,nil,Xx2))).
% 3.33/3.64 all Xx1 (satisfiable_fails(Xx1)<-> (all Xx2 true_fails(Xx1,nil,Xx2))).
% 3.33/3.64 all Xx1 (satisfiable_terminates(Xx1)<-> (all Xx2 true_terminates(Xx1,nil,Xx2))).
% 3.33/3.64 all Xx1 (valid_succeeds(Xx1)<->satisfiable_fails(neg(Xx1))).
% 3.33/3.64 all Xx1 (valid_fails(Xx1)<->satisfiable_succeeds(neg(Xx1))).
% 3.33/3.64 all Xx1 (valid_terminates(Xx1)<->satisfiable_terminates(neg(Xx1))&gr(neg(Xx1))).
% 3.33/3.64 all Xx1 (incon_succeeds(Xx1)<-> (exists Xx2 (member_succeeds(p(Xx2),Xx1)&member_succeeds(neg(p(Xx2)),Xx1)))).
% 3.33/3.64 all Xx1 (incon_fails(Xx1)<-> (all Xx2 (member_fails(p(Xx2),Xx1)|member_fails(neg(p(Xx2)),Xx1)))).
% 3.33/3.64 all Xx1 (incon_terminates(Xx1)<-> (all Xx2 (member_terminates(p(Xx2),Xx1)& (member_fails(p(Xx2),Xx1)|member_terminates(neg(p(Xx2)),Xx1))))).
% 3.33/3.64 all Xx1 (interpretation_succeeds(Xx1)<->literal_list_succeeds(Xx1)&incon_fails(Xx1)).
% 3.33/3.64 all Xx1 (interpretation_fails(Xx1)<->literal_list_fails(Xx1)|incon_succeeds(Xx1)).
% 3.33/3.64 all Xx1 (interpretation_terminates(Xx1)<->literal_list_terminates(Xx1)& (literal_list_fails(Xx1)|incon_terminates(Xx1)&gr(Xx1))).
% 3.33/3.64 all Xx1 (literal_list_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=cons(Xx2,Xx3)&literal_succeeds(Xx2)&literal_list_succeeds(Xx3)))|Xx1=nil).
% 3.33/3.64 all Xx1 (literal_list_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|literal_fails(Xx2)|literal_list_fails(Xx3)))&Xx1!=nil).
% 3.33/3.64 all Xx1 (literal_list_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|literal_terminates(Xx2)& (literal_fails(Xx2)|literal_list_terminates(Xx3))))).
% 3.33/3.64 all Xx1 (literal_succeeds(Xx1)<-> (exists Xx2 (Xx1=neg(p(Xx2))))| (exists Xx3 (Xx1=p(Xx3)))).
% 3.33/3.64 all Xx1 (literal_fails(Xx1)<-> (all Xx2 (Xx1!=neg(p(Xx2))))& (all Xx3 (Xx1!=p(Xx3)))).
% 3.33/3.64 all Xx1 (literal_terminates(Xx1)<-> (all Xx2 $T)& (all Xx3 $T)).
% 3.33/3.64 all Xx1 (formula_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=or(Xx2,Xx3)&formula_succeeds(Xx2)&formula_succeeds(Xx3)))| (exists Xx4 Xx5 (Xx1=and(Xx4,Xx5)&formula_succeeds(Xx4)&formula_succeeds(Xx5)))| (exists Xx6 (Xx1=neg(Xx6)&formula_succeeds(Xx6)))| (exists Xx7 (Xx1=p(Xx7)))).
% 3.33/3.64 all Xx1 (formula_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=or(Xx2,Xx3)|formula_fails(Xx2)|formula_fails(Xx3)))& (all Xx4 Xx5 (Xx1!=and(Xx4,Xx5)|formula_fails(Xx4)|formula_fails(Xx5)))& (all Xx6 (Xx1!=neg(Xx6)|formula_fails(Xx6)))& (all Xx7 (Xx1!=p(Xx7)))).
% 3.33/3.64 all Xx1 (formula_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=or(Xx2,Xx3)|formula_terminates(Xx2)& (formula_fails(Xx2)|formula_terminates(Xx3))))& (all Xx4 Xx5 (Xx1!=and(Xx4,Xx5)|formula_terminates(Xx4)& (formula_fails(Xx4)|formula_terminates(Xx5))))& (all Xx6 (Xx1!=neg(Xx6)|formula_terminates(Xx6)))& (all Xx7 $T)).
% 3.33/3.64 all Xx1 Xx2 (member_succeeds(Xx1,Xx2)<-> (exists Xx3 Xx4 (Xx2=cons(Xx3,Xx4)&member_succeeds(Xx1,Xx4)))| (exists Xx5 (Xx2=cons(Xx1,Xx5)))).
% 3.33/3.64 all Xx1 Xx2 (member_fails(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx2!=cons(Xx3,Xx4)|member_fails(Xx1,Xx4)))& (all Xx5 (Xx2!=cons(Xx1,Xx5)))).
% 3.33/3.64 all Xx1 Xx2 (member_terminates(Xx1,Xx2)<-> (all Xx3 Xx4 (Xx2!=cons(Xx3,Xx4)|member_terminates(Xx1,Xx4)))& (all Xx5 $T)).
% 3.33/3.64 all Xx1 (list_succeeds(Xx1)<-> (exists Xx2 Xx3 (Xx1=cons(Xx2,Xx3)&list_succeeds(Xx3)))|Xx1=nil).
% 3.33/3.64 all Xx1 (list_fails(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|list_fails(Xx3)))&Xx1!=nil).
% 3.33/3.64 all Xx1 (list_terminates(Xx1)<-> (all Xx2 Xx3 (Xx1!=cons(Xx2,Xx3)|list_terminates(Xx3)))).
% 3.33/3.64 all Xl1 Xl2 (sub(Xl1,Xl2)<-> (all Xx (member_succeeds(Xx,Xl1)->member_succeeds(Xx,Xl2)))).
% 3.33/3.64 all Xx Xl (list_succeeds(Xl)->member_terminates(Xx,Xl)).
% 3.33/3.64 all Xx Xy Xl (member_succeeds(Xx,cons(Xy,Xl))&Xx!=Xy->member_succeeds(Xx,Xl)).
% 3.33/3.64 all Xx Xi sub(Xi,cons(Xx,Xi)).
% 3.33/3.64 all Xi Xj Xk (sub(Xi,Xj)&sub(Xj,Xk)->sub(Xi,Xk)).
% 3.33/3.64 all Xl sub(nil,Xl).
% 3.33/3.64 all Xx Xi Xj (sub(Xi,Xj)&member_succeeds(Xx,Xj)->sub(cons(Xx,Xi),Xj)).
% 3.33/3.64 all Xi (list_succeeds(Xi)->incon_terminates(Xi)).
% 3.33/3.64 all Xi (literal_list_succeeds(Xi)->list_succeeds(Xi)).
% 3.33/3.64 all Xi (interpretation_succeeds(Xi)->literal_list_succeeds(Xi)& -(exists Xx (member_succeeds(p(Xx),Xi)&member_succeeds(neg(p(Xx)),Xi)))).
% 3.33/3.64 all Xi (literal_list_succeeds(Xi)& -(exists Xx (member_succeeds(p(Xx),Xi)&member_succeeds(neg(p(Xx)),Xi)))->interpretation_succeeds(Xi)).
% 3.33/3.64 all Xx Xi (interpretation_succeeds(Xi)& -member_succeeds(neg(p(Xx)),Xi)->interpretation_succeeds(cons(p(Xx),Xi))).
% 3.33/3.64 all Xx Xi (interpretation_succeeds(Xi)&member_fails(neg(p(Xx)),Xi)->interpretation_succeeds(cons(p(Xx),Xi))).
% 3.33/3.64 all Xx Xi (interpretation_succeeds(Xi)& -member_succeeds(p(Xx),Xi)->interpretation_succeeds(cons(neg(p(Xx)),Xi))).
% 3.33/3.64 all Xx Xi (interpretation_succeeds(Xi)&member_fails(p(Xx),Xi)->interpretation_succeeds(cons(neg(p(Xx)),Xi))).
% 3.33/3.64 interpretation_succeeds(nil).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)-> (interpretation_succeeds(Xi)->interpretation_succeeds(Xj))& (literal_list_succeeds(Xi)->literal_list_succeeds(Xj))&sub(Xi,Xj)).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)-> (interpretation_succeeds(Xi)->interpretation_succeeds(Xj))& (literal_list_succeeds(Xi)->literal_list_succeeds(Xj))&sub(Xi,Xj)).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)&interpretation_succeeds(Xi)->interpretation_succeeds(Xj)).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)&interpretation_succeeds(Xi)->interpretation_succeeds(Xj)).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)&literal_list_succeeds(Xi)->literal_list_succeeds(Xj)).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)&literal_list_succeeds(Xi)->literal_list_succeeds(Xj)).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)->sub(Xi,Xj)).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)->sub(Xi,Xj)).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj))).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)-> (gr(Xa)&gr(Xi)->gr(Xj))).
% 3.33/3.64 all Xa Xi Xj (true_succeeds(Xa,Xi,Xj)&gr(Xa)&gr(Xi)->gr(Xj)).
% 3.33/3.64 all Xa Xi Xj (false_succeeds(Xa,Xi,Xj)&gr(Xa)&gr(Xi)->gr(Xj)).
% 3.33/3.64 all Xa (formula_succeeds(Xa)-> (all Xi Xj (gr(Xa)&literal_list_succeeds(Xi)&gr(Xi)->true_terminates(Xa,Xi,Xj)&false_terminates(Xa,Xi,Xj)))).
% 3.33/3.64 all Xa (formula_succeeds(Xa)&gr(Xa)->satisfiable_terminates(Xa)).
% 3.33/3.64 all Xa (formula_succeeds(Xa)&gr(Xa)->valid_terminates(Xa)).
% 3.33/3.64 all Xa (formula_succeeds(Xa)-> (all Xi Xx (list_succeeds(Xi)->eval_terminates(Xa,Xi,Xx)))).
% 3.33/3.64 all Xa Xi Xx (eval_succeeds(Xa,Xi,Xx)-> (all Xj (sub(Xi,Xj)->eval_succeeds(Xa,Xj,Xx)))).
% 3.33/3.64 all Xa Xi Xj Xx (eval_succeeds(Xa,Xi,Xx)&sub(Xi,Xj)->eval_succeeds(Xa,Xj,Xx)).
% 3.33/3.64 all Xa Xi Xx (eval_succeeds(Xa,Xi,Xx)-> (interpretation_succeeds(Xi)-> (all Xy (eval_succeeds(Xa,Xi,Xy)->Xx=Xy)))).
% 3.33/3.64 all Xa Xi (defined_succeeds(Xa,Xi)-> (all Xj (sub(Xi,Xj)->defined_succeeds(Xa,Xj)))).
% 3.33/3.64 all Xa Xi Xj (defined_succeeds(Xa,Xi)&sub(Xi,Xj)->defined_succeeds(Xa,Xj)).
% 3.33/3.64 all Xa (valid_fails(Xa)<-> (exists Xi false_succeeds(Xa,nil,Xi))).
% 3.33/3.64 end_of_list.
% 3.33/3.64
% 3.33/3.64 ======= end of input processing =======
% 3.33/3.64
% 3.33/3.64 24 input errors were found.
% 3.33/3.64
% 3.33/3.64 24 input errors were found.
% 3.33/3.64 Otter interrupted
% 3.33/3.64 PROOF NOT FOUND
%------------------------------------------------------------------------------