%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYO634-1 : TPTP v8.2.0. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n026.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 : Mon Jun 24 20:27:33 EDT 2024
% Result : Unsatisfiable 0.54s 0.65s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO634-1 : TPTP v8.2.0. Released v7.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jun 23 09:17:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 0.54/0.64 %-------------------------------------------
% 0.54/0.64 % File :CSE---1.7
% 0.54/0.64 % Problem :theBenchmark
% 0.54/0.64 % Transform :cnf
% 0.54/0.64 % Format :tptp:raw
% 0.54/0.64 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.64
% 0.54/0.64 % Result :Theorem 0.020000s
% 0.54/0.64 % Output :CNFRefutation 0.020000s
% 0.54/0.64 %-------------------------------------------
% 0.54/0.64 %------------------------------------------------------------------------------
% 0.54/0.64 % File : SYO634-1 : TPTP v8.2.0. Released v7.1.0.
% 0.54/0.64 % Domain : Syntactic
% 0.54/0.64 % Problem : NDClauseSet10
% 0.54/0.64 % Version : Especial.
% 0.54/0.64 % English :
% 0.54/0.64
% 0.54/0.64 % Refs : [Cer15] Cerna (2015), Advances in Schematic Cut Elimination
% 0.54/0.64 % : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0
% 0.54/0.64 % : [Cer17] Cerna (2017), Email to Geoff Sutcliffe
% 0.54/0.64 % Source : [Cer17]
% 0.54/0.64 % Names : NDClauseSet10 [Cer17]
% 0.54/0.64
% 0.54/0.64 % Status : Unsatisfiable
% 0.54/0.64 % Rating : 0.09 v8.2.0, 0.00 v7.1.0
% 0.54/0.64 % Syntax : Number of clauses : 23 ( 4 unt; 0 nHn; 5 RR)
% 0.54/0.64 % Number of literals : 141 ( 0 equ; 119 neg)
% 0.54/0.64 % Maximal clause size : 11 ( 6 avg)
% 0.54/0.64 % Maximal term depth : 14 ( 4 avg)
% 0.54/0.64 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty)
% 0.54/0.64 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% 0.54/0.64 % Number of variables : 139 ( 126 sgn)
% 0.54/0.64 % SPC : CNF_UNS_RFO_NEQ_HRN
% 0.54/0.64
% 0.54/0.64 % Comments :
% 0.54/0.64 %------------------------------------------------------------------------------
% 0.54/0.64 cnf(clause_21_01,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | 'E'(f(B_0),s(s(s(s(s(s(s(s('0'))))))))) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_14_02,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(A_8),s('0'))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_7),s(s('0')))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'LEQ'('AP'('0',K),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_11_03,axiom,
% 0.54/0.64 'E'(f(B),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_4_04,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'LEQ'('AP'(s(s('0')),K),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_7_05,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | 'LEQ'('AP'(s(s(s(s(s(s(s(s('0')))))))),K),B_0) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_1_06,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | 'E'(f(B_0),s(s(s(s(s(s('0'))))))) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_5_07,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'LEQ'('AP'(s(s(s('0'))),K),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_20_08,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'LEQ'('AP'(s(s(s(s('0')))),K),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_17_09,axiom,
% 0.54/0.64 'E'(f(B_0),s(s(s(s(s(s(s(s(s('0')))))))))) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_16_10,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_7),s(s('0')))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'LEQ'('AP'(s('0'),K),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_8_11,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_7),s(s('0')))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s('0')) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_9_12,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s(s('0'))))) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_6_13,axiom,
% 0.54/0.64 'LEQ'('AP'(s(s(s(s(s(s(s(s(s('0'))))))))),K),B_0) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_12_14,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | 'E'(f(B_0),s(s(s(s(s(s(s('0')))))))) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_18_15,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.64 | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s('0')))) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_2_16,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.64 | 'LEQ'('AP'(s(s(s(s(s(s('0')))))),K),B_0) ) ).
% 0.54/0.64
% 0.54/0.64 cnf(clause_3_17,axiom,
% 0.54/0.64 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.64 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.64 | ~ 'E'(f(A_8),s('0'))
% 0.54/0.64 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.64 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.64 | ~ 'E'(f(A_7),s(s('0')))
% 0.54/0.64 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.65 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.65 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.65 | ~ 'E'(f(A_9),'0') ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_13_18,axiom,
% 0.54/0.65 ( ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.65 | ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.65 | 'LEQ'('AP'(s(s(s(s(s(s(s('0'))))))),K),B_0) ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_0_19,axiom,
% 0.54/0.65 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.65 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.65 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.65 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.65 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.65 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.65 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.65 | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s('0'))) ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_15_20,axiom,
% 0.54/0.65 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.65 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.65 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.65 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.65 | 'E'(f(B_0),s(s(s(s(s('0')))))) ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_22_21,axiom,
% 0.54/0.65 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.65 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.65 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.65 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.65 | 'LEQ'('AP'(s(s(s(s(s('0'))))),K),B_0) ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_10_22,axiom,
% 0.54/0.65 ( ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
% 0.54/0.65 | ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
% 0.54/0.65 | ~ 'E'(f(A_8),s('0'))
% 0.54/0.65 | ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
% 0.54/0.65 | ~ 'E'(f(A_5),s(s(s(s('0')))))
% 0.54/0.65 | ~ 'E'(f(A_7),s(s('0')))
% 0.54/0.65 | ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
% 0.54/0.65 | ~ 'E'(f(A_6),s(s(s('0'))))
% 0.54/0.65 | ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
% 0.54/0.65 | ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
% 0.54/0.65 | 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),'0') ) ).
% 0.54/0.65
% 0.54/0.65 cnf(clause_19_23,axiom,
% 0.54/0.65 'LEQ'('AP'(s(s(s(s(s(s(s(s(s(s('0')))))))))),K),B) ).
% 0.54/0.65
% 0.54/0.65 %------------------------------------------------------------------------------
% 0.54/0.65 %-------------------------------------------
% 0.54/0.65 % Proof found
% 0.54/0.65 % SZS status Theorem for theBenchmark
% 0.54/0.65 % SZS output start Proof
% 0.54/0.65 %ClaNum:23(EqnAxiom:0)
% 0.54/0.65 %VarNum:152(SingletonVarNum:139)
% 0.54/0.65 %MaxLitNum:11
% 0.54/0.65 %MaxfuncDepth:13
% 0.54/0.65 %SharedTerms:12
% 0.54/0.65 [1]P1(f1(x11),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))
% 0.54/0.65 [2]P1(f1(x21),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [3]P2(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))),x31),x32)
% 0.54/0.65 [4]P2(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))),x41),x42)
% 0.54/0.65 [5]P1(f1(x51),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x52),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x51),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [6]P2(f3(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))),x61),x62)+~P1(f1(x63),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x62),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [7]P1(f1(x71),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x72),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x73),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x71),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [8]P2(f3(f4(f4(f4(f4(f4(f4(f4(a2))))))),x81),x82)+~P1(f1(x83),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x84),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x82),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [9]P1(f1(x91),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x92),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x93),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x94),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x91),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [10]P2(f3(f4(f4(f4(f4(f4(f4(a2)))))),x101),x102)+~P1(f1(x103),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x104),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x105),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x102),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [11]P1(f1(x111),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x112),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x113),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x114),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x115),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x111),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [12]P2(f3(f4(f4(f4(f4(f4(a2))))),x121),x122)+~P1(f1(x123),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x124),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x125),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x126),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x122),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [14]~P1(f1(x142),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x143),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x144),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x145),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x146),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x147),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P2(f3(f4(f4(f4(f4(a2)))),x141),f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x141))
% 0.54/0.65 [19]~P1(f1(x192),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x193),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x194),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x195),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x196),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x197),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x191)),f4(f4(f4(f4(a2)))))
% 0.54/0.65 [15]~P1(f1(x152),f4(f4(f4(f4(a2)))))+~P1(f1(x153),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x154),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x155),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x156),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x157),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x158),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P2(f3(f4(f4(f4(a2))),x151),f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x151))
% 0.54/0.65 [20]~P1(f1(x202),f4(f4(f4(f4(a2)))))+~P1(f1(x203),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x204),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x205),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x206),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x207),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x208),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x201)),f4(f4(f4(a2))))
% 0.54/0.65 [16]~P1(f1(x162),f4(f4(f4(a2))))+~P1(f1(x163),f4(f4(f4(f4(a2)))))+~P1(f1(x164),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x165),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x166),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x167),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x168),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x169),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P2(f3(f4(f4(a2)),x161),f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x161))
% 0.54/0.65 [21]~P1(f1(x212),f4(f4(f4(a2))))+~P1(f1(x213),f4(f4(f4(f4(a2)))))+~P1(f1(x214),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x215),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x216),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x217),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x218),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x219),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x211)),f4(f4(a2)))
% 0.54/0.65 [17]~P1(f1(x172),f4(f4(a2)))+~P1(f1(x173),f4(f4(f4(a2))))+~P1(f1(x174),f4(f4(f4(f4(a2)))))+~P1(f1(x175),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x176),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x177),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x178),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x179),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x1710),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P2(f3(f4(a2),x171),f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x171))
% 0.54/0.65 [22]~P1(f1(x222),f4(f4(a2)))+~P1(f1(x223),f4(f4(f4(a2))))+~P1(f1(x224),f4(f4(f4(f4(a2)))))+~P1(f1(x225),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x226),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x227),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x228),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x229),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x2210),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x221)),f4(a2))
% 0.54/0.65 [13]~P1(f1(x132),f4(a2))+~P1(f1(x131),a2)+~P1(f1(x133),f4(f4(a2)))+~P1(f1(x134),f4(f4(f4(a2))))+~P1(f1(x135),f4(f4(f4(f4(a2)))))+~P1(f1(x136),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x137),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x138),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x139),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x1310),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x1311),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))
% 0.54/0.65 [18]~P1(f1(x182),f4(a2))+~P1(f1(x183),f4(f4(a2)))+~P1(f1(x184),f4(f4(f4(a2))))+~P1(f1(x185),f4(f4(f4(f4(a2)))))+~P1(f1(x186),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x187),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x188),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x189),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x1810),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x1811),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P2(f3(a2,x181),f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x181))
% 0.54/0.65 [23]~P1(f1(x232),f4(a2))+~P1(f1(x233),f4(f4(a2)))+~P1(f1(x234),f4(f4(f4(a2))))+~P1(f1(x235),f4(f4(f4(f4(a2)))))+~P1(f1(x236),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x237),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x238),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x239),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x2310),f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))+~P1(f1(x2311),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x231)),a2)
% 0.54/0.65 %EqnAxiom
% 0.54/0.65
% 0.54/0.65 %-------------------------------------------
% 0.54/0.65 cnf(24,plain,
% 0.54/0.65 (P1(f1(x241),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x241),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))),
% 0.54/0.65 inference(scs_inference,[],[1,5])).
% 0.54/0.65 cnf(25,plain,
% 0.54/0.65 (P1(f1(x251),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x252),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x251),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))),
% 0.54/0.65 inference(scs_inference,[],[1,7])).
% 0.54/0.65 cnf(26,plain,
% 0.54/0.65 (P1(f1(x261),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x262),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x263),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x261),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))),
% 0.54/0.65 inference(scs_inference,[],[1,9])).
% 0.54/0.65 cnf(27,plain,
% 0.54/0.65 (P1(f1(x271),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x272),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x273),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x274),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x271),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))),
% 0.54/0.65 inference(scs_inference,[],[1,11])).
% 0.54/0.65 cnf(28,plain,
% 0.54/0.65 (~P1(f1(x281),f4(a2))+~P1(f1(x282),a2)+~P1(f1(x283),f4(f4(a2)))+~P1(f1(x284),f4(f4(f4(a2))))+~P1(f1(x285),f4(f4(f4(f4(a2)))))+~P1(f1(x286),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x287),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x288),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x289),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))),
% 0.54/0.65 inference(scs_inference,[],[2,1,13])).
% 0.54/0.65 cnf(29,plain,
% 0.54/0.65 (~P1(f1(x291),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x292),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x293),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x294),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x295)),f4(f4(f4(f4(a2)))))),
% 0.54/0.65 inference(scs_inference,[],[2,1,19])).
% 0.54/0.65 cnf(30,plain,
% 0.54/0.65 (~P1(f1(x301),f4(f4(f4(f4(a2)))))+~P1(f1(x302),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x303),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x304),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x305),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x306)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[2,1,20])).
% 0.54/0.65 cnf(31,plain,
% 0.54/0.65 (~P1(f1(x311),f4(f4(f4(a2))))+~P1(f1(x312),f4(f4(f4(f4(a2)))))+~P1(f1(x313),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x314),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x315),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x316),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x317)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[2,1,21])).
% 0.54/0.65 cnf(32,plain,
% 0.54/0.65 (~P1(f1(x321),f4(f4(a2)))+~P1(f1(x322),f4(f4(f4(a2))))+~P1(f1(x323),f4(f4(f4(f4(a2)))))+~P1(f1(x324),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x325),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x326),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x327),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x328)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[2,1,22])).
% 0.54/0.65 cnf(33,plain,
% 0.54/0.65 (~P1(f1(x331),f4(a2))+~P1(f1(x332),f4(f4(a2)))+~P1(f1(x333),f4(f4(f4(a2))))+~P1(f1(x334),f4(f4(f4(f4(a2)))))+~P1(f1(x335),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x336),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x337),f4(f4(f4(f4(f4(f4(f4(a2))))))))+~P1(f1(x338),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x339)),a2)),
% 0.54/0.65 inference(scs_inference,[],[2,1,23])).
% 0.54/0.65 cnf(34,plain,
% 0.54/0.65 (P1(f1(x341),f4(f4(f4(f4(f4(f4(f4(a2))))))))),
% 0.54/0.65 inference(scs_inference,[],[2,24,25])).
% 0.54/0.65 cnf(35,plain,
% 0.54/0.65 (~P1(f1(x351),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+~P1(f1(x352),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(x351),f4(f4(f4(f4(f4(f4(a2)))))))),
% 0.54/0.65 inference(scs_inference,[],[34,26])).
% 0.54/0.65 cnf(36,plain,
% 0.54/0.65 (~P1(f1(x361),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+~P1(f1(x362),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x363),f4(f4(f4(f4(f4(f4(a2)))))))+P1(f1(x361),f4(f4(f4(f4(f4(a2))))))),
% 0.54/0.65 inference(scs_inference,[],[34,27])).
% 0.54/0.65 cnf(37,plain,
% 0.54/0.65 (~P1(f1(x371),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x372),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x373),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x374),f4(f4(f4(f4(a2)))))+~P1(f1(x375),f4(f4(f4(a2))))+~P1(f1(x376),f4(f4(a2)))+~P1(f1(x377),f4(a2))+~P1(f1(x378),a2)),
% 0.54/0.65 inference(scs_inference,[],[34,28])).
% 0.54/0.65 cnf(38,plain,
% 0.54/0.65 (~P1(f1(x381),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x382),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x383),f4(f4(f4(f4(f4(a2))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x384)),f4(f4(f4(f4(a2)))))),
% 0.54/0.65 inference(scs_inference,[],[34,29])).
% 0.54/0.65 cnf(39,plain,
% 0.54/0.65 (~P1(f1(x391),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x392),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x393),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x394),f4(f4(f4(f4(a2)))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x395)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[34,30])).
% 0.54/0.65 cnf(40,plain,
% 0.54/0.65 (~P1(f1(x401),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x402),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x403),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x404),f4(f4(f4(f4(a2)))))+~P1(f1(x405),f4(f4(f4(a2))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x406)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[34,31])).
% 0.54/0.65 cnf(41,plain,
% 0.54/0.65 (~P1(f1(x411),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x412),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x413),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x414),f4(f4(f4(f4(a2)))))+~P1(f1(x415),f4(f4(f4(a2))))+~P1(f1(x416),f4(f4(a2)))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x417)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[34,32])).
% 0.54/0.65 cnf(42,plain,
% 0.54/0.65 (~P1(f1(x421),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x422),f4(f4(f4(f4(f4(f4(a2)))))))+~P1(f1(x423),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x424),f4(f4(f4(f4(a2)))))+~P1(f1(x425),f4(f4(f4(a2))))+~P1(f1(x426),f4(f4(a2)))+~P1(f1(x427),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x428)),a2)),
% 0.54/0.65 inference(scs_inference,[],[34,33])).
% 0.54/0.65 cnf(43,plain,
% 0.54/0.65 (P1(f1(x431),f4(f4(f4(f4(f4(f4(a2)))))))),
% 0.54/0.65 inference(scs_inference,[],[2,35,24])).
% 0.54/0.65 cnf(44,plain,
% 0.54/0.65 (~P1(f1(x441),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))))+~P1(f1(x442),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(x441),f4(f4(f4(f4(f4(a2))))))),
% 0.54/0.65 inference(scs_inference,[],[43,36])).
% 0.54/0.65 cnf(45,plain,
% 0.54/0.65 (~P1(f1(x451),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x452),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x453),f4(f4(f4(f4(a2)))))+~P1(f1(x454),f4(f4(f4(a2))))+~P1(f1(x455),f4(f4(a2)))+~P1(f1(x456),f4(a2))+~P1(f1(x457),a2)),
% 0.54/0.65 inference(scs_inference,[],[43,37])).
% 0.54/0.65 cnf(46,plain,
% 0.54/0.65 (~P1(f1(x461),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x462),f4(f4(f4(f4(f4(a2))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x463)),f4(f4(f4(f4(a2)))))),
% 0.54/0.65 inference(scs_inference,[],[43,38])).
% 0.54/0.65 cnf(47,plain,
% 0.54/0.65 (~P1(f1(x471),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x472),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x473),f4(f4(f4(f4(a2)))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x474)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[43,39])).
% 0.54/0.65 cnf(48,plain,
% 0.54/0.65 (~P1(f1(x481),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x482),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x483),f4(f4(f4(f4(a2)))))+~P1(f1(x484),f4(f4(f4(a2))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x485)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[43,40])).
% 0.54/0.65 cnf(49,plain,
% 0.54/0.65 (~P1(f1(x491),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x492),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x493),f4(f4(f4(f4(a2)))))+~P1(f1(x494),f4(f4(f4(a2))))+~P1(f1(x495),f4(f4(a2)))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x496)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[43,41])).
% 0.54/0.65 cnf(50,plain,
% 0.54/0.65 (~P1(f1(x501),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x502),f4(f4(f4(f4(f4(a2))))))+~P1(f1(x503),f4(f4(f4(f4(a2)))))+~P1(f1(x504),f4(f4(f4(a2))))+~P1(f1(x505),f4(f4(a2)))+~P1(f1(x506),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x507)),a2)),
% 0.54/0.65 inference(scs_inference,[],[43,42])).
% 0.54/0.65 cnf(51,plain,
% 0.54/0.65 (P1(f1(x511),f4(f4(f4(f4(f4(a2))))))),
% 0.54/0.65 inference(scs_inference,[],[2,44,24])).
% 0.54/0.65 cnf(52,plain,
% 0.54/0.65 (~P1(f1(x521),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x522),f4(f4(f4(f4(a2)))))+~P1(f1(x523),f4(f4(f4(a2))))+~P1(f1(x524),f4(f4(a2)))+~P1(f1(x525),f4(a2))+~P1(f1(x526),a2)),
% 0.54/0.65 inference(scs_inference,[],[51,45])).
% 0.54/0.65 cnf(53,plain,
% 0.54/0.65 (~P1(f1(x531),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x532)),f4(f4(f4(f4(a2)))))),
% 0.54/0.65 inference(scs_inference,[],[51,46])).
% 0.54/0.65 cnf(54,plain,
% 0.54/0.65 (~P1(f1(x541),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x542),f4(f4(f4(f4(a2)))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x543)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[51,47])).
% 0.54/0.65 cnf(55,plain,
% 0.54/0.65 (~P1(f1(x551),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x552),f4(f4(f4(f4(a2)))))+~P1(f1(x553),f4(f4(f4(a2))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x554)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[51,48])).
% 0.54/0.65 cnf(56,plain,
% 0.54/0.65 (~P1(f1(x561),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x562),f4(f4(f4(f4(a2)))))+~P1(f1(x563),f4(f4(f4(a2))))+~P1(f1(x564),f4(f4(a2)))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x565)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[51,49])).
% 0.54/0.65 cnf(57,plain,
% 0.54/0.65 (~P1(f1(x571),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x572),f4(f4(f4(f4(a2)))))+~P1(f1(x573),f4(f4(f4(a2))))+~P1(f1(x574),f4(f4(a2)))+~P1(f1(x575),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x576)),a2)),
% 0.54/0.65 inference(scs_inference,[],[51,50])).
% 0.54/0.65 cnf(58,plain,
% 0.54/0.65 (P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x581)),f4(f4(f4(f4(a2)))))),
% 0.54/0.65 inference(scs_inference,[],[2,53,24])).
% 0.54/0.65 cnf(59,plain,
% 0.54/0.65 (~P1(f1(x591),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x592),f4(f4(f4(a2))))+~P1(f1(x593),f4(f4(a2)))+~P1(f1(x594),f4(a2))+~P1(f1(x595),a2)),
% 0.54/0.65 inference(scs_inference,[],[58,52])).
% 0.54/0.65 cnf(60,plain,
% 0.54/0.65 (~P1(f1(x601),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x602)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[58,54])).
% 0.54/0.65 cnf(61,plain,
% 0.54/0.65 (~P1(f1(x611),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x612),f4(f4(f4(a2))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x613)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[58,55])).
% 0.54/0.65 cnf(62,plain,
% 0.54/0.65 (~P1(f1(x621),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x622),f4(f4(f4(a2))))+~P1(f1(x623),f4(f4(a2)))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x624)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[58,56])).
% 0.54/0.65 cnf(63,plain,
% 0.54/0.65 (~P1(f1(x631),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x632),f4(f4(f4(a2))))+~P1(f1(x633),f4(f4(a2)))+~P1(f1(x634),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x635)),a2)),
% 0.54/0.65 inference(scs_inference,[],[58,57])).
% 0.54/0.65 cnf(64,plain,
% 0.54/0.65 (P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x641)),f4(f4(f4(a2))))),
% 0.54/0.65 inference(scs_inference,[],[2,60,24])).
% 0.54/0.65 cnf(65,plain,
% 0.54/0.65 (~P1(f1(x651),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x652),f4(f4(a2)))+~P1(f1(x653),f4(a2))+~P1(f1(x654),a2)),
% 0.54/0.65 inference(scs_inference,[],[64,59])).
% 0.54/0.65 cnf(66,plain,
% 0.54/0.65 (~P1(f1(x661),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x662)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[64,61])).
% 0.54/0.65 cnf(67,plain,
% 0.54/0.65 (~P1(f1(x671),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x672),f4(f4(a2)))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x673)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[64,62])).
% 0.54/0.65 cnf(68,plain,
% 0.54/0.65 (~P1(f1(x681),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x682),f4(f4(a2)))+~P1(f1(x683),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x684)),a2)),
% 0.54/0.65 inference(scs_inference,[],[64,63])).
% 0.54/0.65 cnf(69,plain,
% 0.54/0.65 (P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x691)),f4(f4(a2)))),
% 0.54/0.65 inference(scs_inference,[],[2,66,24])).
% 0.54/0.65 cnf(70,plain,
% 0.54/0.65 (~P1(f1(x701),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x702),f4(a2))+~P1(f1(x703),a2)),
% 0.54/0.65 inference(scs_inference,[],[69,65])).
% 0.54/0.65 cnf(71,plain,
% 0.54/0.65 (~P1(f1(x711),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x712)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[69,67])).
% 0.54/0.65 cnf(72,plain,
% 0.54/0.65 (~P1(f1(x721),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x722),f4(a2))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x723)),a2)),
% 0.54/0.65 inference(scs_inference,[],[69,68])).
% 0.54/0.65 cnf(73,plain,
% 0.54/0.65 (P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x731)),f4(a2))),
% 0.54/0.65 inference(scs_inference,[],[2,71,24])).
% 0.54/0.65 cnf(74,plain,
% 0.54/0.65 (~P1(f1(x741),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+~P1(f1(x742),a2)),
% 0.54/0.65 inference(scs_inference,[],[73,70])).
% 0.54/0.65 cnf(75,plain,
% 0.54/0.65 (~P1(f1(x751),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))+P1(f1(f3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a2))))))))))),x752)),a2)),
% 0.54/0.65 inference(scs_inference,[],[73,72])).
% 0.54/0.65 cnf(76,plain,
% 0.54/0.65 (~P1(f1(x761),a2)),
% 0.54/0.65 inference(scs_inference,[],[2,74,24])).
% 0.54/0.65 cnf(77,plain,
% 0.54/0.65 (~P1(f1(x771),f4(f4(f4(f4(f4(f4(f4(f4(a2)))))))))),
% 0.54/0.65 inference(scs_inference,[],[76,75])).
% 0.54/0.65 cnf(78,plain,
% 0.54/0.65 ($false),
% 0.54/0.65 inference(scs_inference,[],[77,2,24]),
% 0.54/0.65 ['proof']).
% 0.54/0.65 % SZS output end Proof
% 0.54/0.65 % Total time :0.020000s
%------------------------------------------------------------------------------