Leo-III---1.8.0.CAX-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : SYO904^12 : TPTP v9.3.1. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39

% Computer : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Sep 30 08:46:13 AM UTC 2026

% Result   : ContradictoryAxioms 87.32s 39.31s
% Output   : Refutation 88.18s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYO904^12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20  % Computer : n019.cluster.edu
% 0.09/0.20  % Model    : x86_64 x86_64
% 0.09/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20  % Memory   : 8046.5625MB
% 0.09/0.20  % OS       : Linux 6.8.0-71-generic
% 0.09/0.20  % CPULimit : 300
% 0.09/0.20  % WCLimit  : 300
% 0.09/0.20  % DateTime : Tue Sep 29 17:26:32 UTC 2026
% 0.09/0.20  % CPUTime  : 
% 0.09/0.20  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.65/0.53  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 1.35/0.74  % [INFO] 	 Parsing done (209ms). 
% 1.35/0.75  % [INFO] 	 Running in sequential loop mode. 
% 2.05/0.98  % [INFO] 	 eprover registered as external prover. 
% 2.05/0.99  % [INFO] 	 Scanning for conjecture ... 
% 2.59/1.17  % [INFO] 	 Found a conjecture (or negated_conjecture) and 52 axioms. Running axiom selection ... 
% 2.81/1.27  % [INFO] 	 Axiom selection finished. Selected 52 axioms (removed 0 axioms). 
% 3.56/1.43  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 3.56/1.44  % [INFO] 	 Type checking passed. 
% 3.56/1.44  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 87.32/39.30  % [INFO] 	 Killing All external provers ... 
% 87.32/39.30  % Time passed: 38994ms (effective reasoning time: 38546ms)
% 87.32/39.31  % Axioms used in derivation (10): mod8, mod4, mod45, mrel_universal, mod49, mod6, alt1, mod34, mod23, mod47
% 87.32/39.31  % No. of inferences in proof: 173
% 87.32/39.31  % SZS status ContradictoryAxioms for /export/starexec/sandbox2/benchmark/theBenchmark.p : 38994 ms resp. 38546 ms w/o parsing
% 88.18/39.56  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 88.18/39.56  thf(mworld_type, type, mworld: $tType).
% 88.18/39.56  thf(mrel_decl, type, mrel: (mworld > (mworld > $o))).
% 88.18/39.56  thf(mactual_decl, type, mactual: mworld).
% 88.18/39.56  thf(mlocal_decl, type, mlocal: ((mworld > $o) > $o)).
% 88.18/39.56  thf(mnot_decl, type, mnot: ((mworld > $o) > (mworld > $o))).
% 88.18/39.56  thf(mand_decl, type, mand: ((mworld > $o) > ((mworld > $o) > (mworld > $o)))).
% 88.18/39.56  thf(mor_decl, type, mor: ((mworld > $o) > ((mworld > $o) > (mworld > $o)))).
% 88.18/39.56  thf(mbox_decl, type, mbox: ((mworld > $o) > (mworld > $o))).
% 88.18/39.56  thf(mdia_decl, type, mdia: ((mworld > $o) > (mworld > $o))).
% 88.18/39.56  thf(v1_decl, type, v1: (mworld > $o)).
% 88.18/39.56  thf(v2_decl, type, v2: (mworld > $o)).
% 88.18/39.56  thf(v3_decl, type, v3: (mworld > $o)).
% 88.18/39.56  thf(v5_decl, type, v5: (mworld > $o)).
% 88.18/39.56  thf(v6_decl, type, v6: (mworld > $o)).
% 88.18/39.56  thf(v7_decl, type, v7: (mworld > $o)).
% 88.18/39.56  thf(v8_decl, type, v8: (mworld > $o)).
% 88.18/39.56  thf(v9_decl, type, v9: (mworld > $o)).
% 88.18/39.56  thf(v14_decl, type, v14: (mworld > $o)).
% 88.18/39.56  thf(v13_decl, type, v13: (mworld > $o)).
% 88.18/39.56  thf(v16_decl, type, v16: (mworld > $o)).
% 88.18/39.56  thf(v15_decl, type, v15: (mworld > $o)).
% 88.18/39.56  thf(v18_decl, type, v18: (mworld > $o)).
% 88.18/39.56  thf(v21_decl, type, v21: (mworld > $o)).
% 88.18/39.56  thf(v23_decl, type, v23: (mworld > $o)).
% 88.18/39.56  thf(v22_decl, type, v22: (mworld > $o)).
% 88.18/39.56  thf(v24_decl, type, v24: (mworld > $o)).
% 88.18/39.56  thf(v26_decl, type, v26: (mworld > $o)).
% 88.18/39.56  thf(v28_decl, type, v28: (mworld > $o)).
% 88.18/39.56  thf(sk1_decl, type, sk1: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))))))))).
% 88.18/39.56  thf(sk2_decl, type, sk2: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))))))))).
% 88.18/39.56  thf(sk3_decl, type, sk3: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))))))).
% 88.18/39.56  thf(sk4_decl, type, sk4: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))))))).
% 88.18/39.56  thf(sk5_decl, type, sk5: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))))).
% 88.18/39.56  thf(sk6_decl, type, sk6: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))))).
% 88.18/39.56  thf(sk7_decl, type, sk7: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))))).
% 88.18/39.56  thf(sk8_decl, type, sk8: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))))).
% 88.18/39.56  thf(sk9_decl, type, sk9: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))).
% 88.18/39.56  thf(sk10_decl, type, sk10: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))))).
% 88.18/39.56  thf(sk11_decl, type, sk11: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))).
% 88.18/39.56  thf(sk12_decl, type, sk12: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))))).
% 88.18/39.56  thf(sk13_decl, type, sk13: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))))).
% 88.18/39.56  thf(sk14_decl, type, sk14: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))).
% 88.18/39.56  thf(sk15_decl, type, sk15: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))).
% 88.18/39.56  thf(sk16_decl, type, sk16: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))).
% 88.18/39.56  thf(sk17_decl, type, sk17: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))).
% 88.18/39.56  thf(sk18_decl, type, sk18: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))).
% 88.18/39.56  thf(sk19_decl, type, sk19: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))).
% 88.18/39.56  thf(sk20_decl, type, sk20: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))).
% 88.18/39.56  thf(sk21_decl, type, sk21: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))).
% 88.18/39.56  thf(sk22_decl, type, sk22: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))).
% 88.18/39.56  thf(sk23_decl, type, sk23: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))).
% 88.18/39.56  thf(sk24_decl, type, sk24: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))).
% 88.18/39.56  thf(sk25_decl, type, sk25: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))).
% 88.18/39.56  thf(sk26_decl, type, sk26: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))).
% 88.18/39.56  thf(sk27_decl, type, sk27: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))).
% 88.18/39.56  thf(sk28_decl, type, sk28: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))).
% 88.18/39.56  thf(sk29_decl, type, sk29: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))).
% 88.18/39.56  thf(sk30_decl, type, sk30: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))).
% 88.18/39.56  thf(sk31_decl, type, sk31: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))).
% 88.18/39.56  thf(sk32_decl, type, sk32: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))).
% 88.18/39.56  thf(sk33_decl, type, sk33: (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))).
% 88.18/39.56  thf(sk34_decl, type, sk34: (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))).
% 88.18/39.56  thf(sk35_decl, type, sk35: (mworld > (mworld > (mworld > (mworld > mworld))))).
% 88.18/39.56  thf(sk36_decl, type, sk36: (mworld > (mworld > (mworld > (mworld > mworld))))).
% 88.18/39.56  thf(sk37_decl, type, sk37: (mworld > (mworld > (mworld > mworld)))).
% 88.18/39.56  thf(sk38_decl, type, sk38: (mworld > (mworld > mworld))).
% 88.18/39.56  thf(sk39_decl, type, sk39: (mworld > mworld)).
% 88.18/39.56  thf(sk40_decl, type, sk40: mworld).
% 88.18/39.56  thf(mlocal_def, definition, mlocal = (^ [A:(mworld > $o)]: (A @ mactual)) ).
% 88.18/39.56  thf(mnot_def, definition, mnot = (^ [A:(mworld > $o),B:mworld]: ~ (A @ B)) ).
% 88.18/39.56  thf(mand_def, definition, mand = (^ [A:(mworld > $o),B:(mworld > $o),C:mworld]: ((A @ C) & (B @ C))) ).
% 88.18/39.56  thf(mor_def, definition, mor = (^ [A:(mworld > $o),B:(mworld > $o),C:mworld]: ((A @ C) | (B @ C))) ).
% 88.18/39.56  thf(mbox_def, definition, mbox = (^ [A:(mworld > $o),B:mworld]: ! [C:mworld]: ((mrel @ B @ C) => (A @ C))) ).
% 88.18/39.56  thf(mdia_def, definition, mdia = (^ [A:(mworld > $o),B:mworld]: ? [C:mworld]: ((mrel @ B @ C) & (A @ C))) ).
% 88.18/39.56  thf(sk1_def, definition, sk1 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld,X:mworld,Y:mworld,Z:mworld,ZA:mworld]: (@+ [ZB:mworld]: (mrel @ A @ ZB))) ).
% 88.18/39.56  thf(sk2_def, definition, sk2 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld,X:mworld,Y:mworld,Z:mworld]: (@+ [ZA:mworld]: (mrel @ A @ ZA))) ).
% 88.18/39.56  thf(sk3_def, definition, sk3 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld,X:mworld,Y:mworld]: (@+ [Z:mworld]: (mrel @ A @ Z))) ).
% 88.18/39.56  thf(sk4_def, definition, sk4 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld,X:mworld]: (@+ [Y:mworld]: (mrel @ A @ Y))) ).
% 88.18/39.56  thf(sk5_def, definition, sk5 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld]: (@+ [X:mworld]: ((mrel @ A @ X) & (v5 @ X)))) ).
% 88.18/39.56  thf(sk6_def, definition, sk6 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld,W:mworld]: (@+ [X:mworld]: ((mrel @ A @ X) & ~ (v5 @ X)))) ).
% 88.18/39.56  thf(sk7_def, definition, sk7 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld]: (@+ [W:mworld]: ((mrel @ A @ W) & (v6 @ W)))) ).
% 88.18/39.56  thf(sk8_def, definition, sk8 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld,V:mworld]: (@+ [W:mworld]: ((mrel @ A @ W) & ~ (v6 @ W)))) ).
% 88.18/39.56  thf(sk9_def, definition, sk9 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld]: (@+ [V:mworld]: ((mrel @ A @ V) & (v7 @ V)))) ).
% 88.18/39.56  thf(sk10_def, definition, sk10 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld,U:mworld]: (@+ [V:mworld]: ((mrel @ A @ V) & ~ (v7 @ V)))) ).
% 88.18/39.56  thf(sk11_def, definition, sk11 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld]: (@+ [U:mworld]: ((mrel @ A @ U) & (v8 @ U)))) ).
% 88.18/39.56  thf(sk12_def, definition, sk12 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld,T:mworld]: (@+ [U:mworld]: ((mrel @ A @ U) & ~ (v8 @ U)))) ).
% 88.18/39.56  thf(sk13_def, definition, sk13 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld,S:mworld]: (@+ [T:mworld]: (mrel @ A @ T))) ).
% 88.18/39.56  thf(sk14_def, definition, sk14 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld,R:mworld]: (@+ [S:mworld]: (mrel @ A @ S))) ).
% 88.18/39.56  thf(sk15_def, definition, sk15 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld,Q:mworld]: (@+ [R:mworld]: (mrel @ A @ R))) ).
% 88.18/39.56  thf(sk16_def, definition, sk16 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld,P:mworld]: (@+ [Q:mworld]: (mrel @ A @ Q))) ).
% 88.18/39.56  thf(sk17_def, definition, sk17 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld]: (@+ [P:mworld]: ((mrel @ A @ P) & (v13 @ P)))) ).
% 88.18/39.56  thf(sk18_def, definition, sk18 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld,O:mworld]: (@+ [P:mworld]: ((mrel @ A @ P) & ~ (v13 @ P)))) ).
% 88.18/39.56  thf(sk19_def, definition, sk19 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld]: (@+ [O:mworld]: ((mrel @ A @ O) & (v14 @ O)))) ).
% 88.18/39.56  thf(sk20_def, definition, sk20 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld,N:mworld]: (@+ [O:mworld]: ((mrel @ A @ O) & ~ (v14 @ O)))) ).
% 88.18/39.56  thf(sk21_def, definition, sk21 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld]: (@+ [N:mworld]: ((mrel @ A @ N) & (v15 @ N)))) ).
% 88.18/39.56  thf(sk22_def, definition, sk22 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld,M:mworld]: (@+ [N:mworld]: ((mrel @ A @ N) & ~ (v15 @ N)))) ).
% 88.18/39.56  thf(sk23_def, definition, sk23 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld]: (@+ [M:mworld]: ((mrel @ A @ M) & (v16 @ M)))) ).
% 88.18/39.56  thf(sk24_def, definition, sk24 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld,L:mworld]: (@+ [M:mworld]: ((mrel @ A @ M) & ~ (v16 @ M)))) ).
% 88.18/39.56  thf(sk25_def, definition, sk25 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld,K:mworld]: (@+ [L:mworld]: (mrel @ A @ L))) ).
% 88.18/39.56  thf(sk26_def, definition, sk26 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld,J:mworld]: (@+ [K:mworld]: (mrel @ A @ K))) ).
% 88.18/39.56  thf(sk27_def, definition, sk27 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld,I:mworld]: (@+ [J:mworld]: (mrel @ A @ J))) ).
% 88.18/39.56  thf(sk28_def, definition, sk28 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld,H:mworld]: (@+ [I:mworld]: (mrel @ A @ I))) ).
% 88.18/39.56  thf(sk29_def, definition, sk29 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld]: (@+ [H:mworld]: ((mrel @ A @ H) & (v21 @ H)))) ).
% 88.18/39.56  thf(sk30_def, definition, sk30 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld,G:mworld]: (@+ [H:mworld]: ((mrel @ A @ H) & ~ (v21 @ H)))) ).
% 88.18/39.56  thf(sk31_def, definition, sk31 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld]: (@+ [G:mworld]: ((mrel @ A @ G) & (v22 @ G)))) ).
% 88.18/39.56  thf(sk32_def, definition, sk32 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld]: (@+ [G:mworld]: ((mrel @ A @ G) & ~ (v22 @ G)))) ).
% 88.18/39.56  thf(sk33_def, definition, sk33 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld]: (@+ [F:mworld]: ((mrel @ A @ F) & (v23 @ F)))) ).
% 88.18/39.56  thf(sk34_def, definition, sk34 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld]: (@+ [F:mworld]: ((mrel @ A @ F) & ~ (v23 @ F)))) ).
% 88.18/39.56  thf(sk35_def, definition, sk35 = (^ [A:mworld,B:mworld,C:mworld,D:mworld]: (@+ [E:mworld]: ((mrel @ A @ E) & (v24 @ E)))) ).
% 88.18/39.56  thf(sk36_def, definition, sk36 = (^ [A:mworld,B:mworld,C:mworld,D:mworld]: (@+ [E:mworld]: ((mrel @ A @ E) & ~ (v24 @ E)))) ).
% 88.18/39.56  thf(sk37_def, definition, sk37 = (^ [A:mworld,B:mworld,C:mworld]: (@+ [D:mworld]: (mrel @ A @ D))) ).
% 88.18/39.56  thf(sk38_def, definition, sk38 = (^ [A:mworld,B:mworld]: (@+ [C:mworld]: (mrel @ A @ C))) ).
% 88.18/39.56  thf(sk39_def, definition, sk39 = (^ [A:mworld]: (@+ [B:mworld]: (mrel @ A @ B))) ).
% 88.18/39.56  thf(sk40_def, definition, sk40 = (@+ [A:mworld]: (mrel @ mactual @ A)) ).
% 88.18/39.56  thf(27,axiom,((mlocal @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mdia @ (^ [A:mworld]: (($true))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mand @ (mdia @ v5) @ (mdia @ (mnot @ v5))))) @ (mand @ (mdia @ v6) @ (mdia @ (mnot @ v6))))) @ (mand @ (mdia @ v7) @ (mdia @ (mnot @ v7))))) @ (mand @ (mdia @ v8) @ (mdia @ (mnot @ v8))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mand @ (mdia @ v13) @ (mdia @ (mnot @ v13))))) @ (mand @ (mdia @ v14) @ (mdia @ (mnot @ v14))))) @ (mand @ (mdia @ v15) @ (mdia @ (mnot @ v15))))) @ (mand @ (mdia @ v16) @ (mdia @ (mnot @ v16))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mand @ (mdia @ v21) @ (mdia @ (mnot @ v21))))) @ (mand @ (mdia @ v22) @ (mdia @ (mnot @ v22))))) @ (mand @ (mdia @ v23) @ (mdia @ (mnot @ v23))))) @ (mand @ (mdia @ v24) @ (mdia @ (mnot @ v24))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true)))))) @ (mdia @ (^ [A:mworld]: (($true))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt1)).
% 88.18/39.56  thf(104,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (! [X:mworld]: ((mrel @ W @ X) => (! [Y:mworld]: ((mrel @ X @ Y) => (! [Z:mworld]: ((mrel @ Y @ Z) => (! [ZA:mworld]: ((mrel @ Z @ ZA) => (? [ZB:mworld]: (mrel @ ZA @ ZB))) & ? [ZA:mworld]: (mrel @ Z @ ZA))) & ? [Z:mworld]: (mrel @ Y @ Z))) & ? [Y:mworld]: (mrel @ X @ Y))) & ? [X:mworld]: ((mrel @ W @ X) & (v5 @ X)) & ? [X:mworld]: ((mrel @ W @ X) & ~ (v5 @ X)))) & ? [W:mworld]: ((mrel @ V @ W) & (v6 @ W)) & ? [W:mworld]: ((mrel @ V @ W) & ~ (v6 @ W)))) & ? [V:mworld]: ((mrel @ U @ V) & (v7 @ V)) & ? [V:mworld]: ((mrel @ U @ V) & ~ (v7 @ V)))) & ? [U:mworld]: ((mrel @ T @ U) & (v8 @ U)) & ? [U:mworld]: ((mrel @ T @ U) & ~ (v8 @ U)))) & ? [T:mworld]: (mrel @ S @ T))) & ? [S:mworld]: (mrel @ R @ S))) & ? [R:mworld]: (mrel @ Q @ R))) & ? [Q:mworld]: (mrel @ P @ Q))) & ? [P:mworld]: ((mrel @ O @ P) & (v13 @ P)) & ? [P:mworld]: ((mrel @ O @ P) & ~ (v13 @ P)))) & ? [O:mworld]: ((mrel @ N @ O) & (v14 @ O)) & ? [O:mworld]: ((mrel @ N @ O) & ~ (v14 @ O)))) & ? [N:mworld]: ((mrel @ M @ N) & (v15 @ N)) & ? [N:mworld]: ((mrel @ M @ N) & ~ (v15 @ N)))) & ? [M:mworld]: ((mrel @ L @ M) & (v16 @ M)) & ? [M:mworld]: ((mrel @ L @ M) & ~ (v16 @ M)))) & ? [L:mworld]: (mrel @ K @ L))) & ? [K:mworld]: (mrel @ J @ K))) & ? [J:mworld]: (mrel @ I @ J))) & ? [I:mworld]: (mrel @ H @ I))) & ? [H:mworld]: ((mrel @ G @ H) & (v21 @ H)) & ? [H:mworld]: ((mrel @ G @ H) & ~ (v21 @ H)))) & ? [G:mworld]: ((mrel @ F @ G) & (v22 @ G)) & ? [G:mworld]: ((mrel @ F @ G) & ~ (v22 @ G)))) & ? [F:mworld]: ((mrel @ E @ F) & (v23 @ F)) & ? [F:mworld]: ((mrel @ E @ F) & ~ (v23 @ F)))) & ? [E:mworld]: ((mrel @ D @ E) & (v24 @ E)) & ? [E:mworld]: ((mrel @ D @ E) & ~ (v24 @ E)))) & ? [D:mworld]: (mrel @ C @ D))) & ? [C:mworld]: (mrel @ B @ C))) & ? [B:mworld]: (mrel @ A @ B))) & ? [A:mworld]: (mrel @ mactual @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 88.18/39.56  thf(105,plain,(! [ZA:mworld,Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (((~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | ~ (mrel @ W @ X) | ~ (mrel @ X @ Y) | ~ (mrel @ Y @ Z) | ~ (mrel @ Z @ ZA) | (mrel @ ZA @ (sk1 @ ZA @ Z @ Y @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | ~ (mrel @ W @ X) | ~ (mrel @ X @ Y) | ~ (mrel @ Y @ Z) | (mrel @ Z @ (sk2 @ Z @ Y @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | ~ (mrel @ W @ X) | ~ (mrel @ X @ Y) | (mrel @ Y @ (sk3 @ Y @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | ~ (mrel @ W @ X) | (mrel @ X @ (sk4 @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | (mrel @ W @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | (v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | (mrel @ W @ (sk6 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (mrel @ V @ W) | ~ (v5 @ (sk6 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | (mrel @ V @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | (v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | (mrel @ V @ (sk8 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (mrel @ U @ V) | ~ (v6 @ (sk8 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | (mrel @ U @ (sk9 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | (v7 @ (sk9 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | (mrel @ U @ (sk10 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (mrel @ T @ U) | ~ (v7 @ (sk10 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | (mrel @ T @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | (v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | (mrel @ T @ (sk12 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | ~ (mrel @ S @ T) | ~ (v8 @ (sk12 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | ~ (mrel @ R @ S) | (mrel @ S @ (sk13 @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | ~ (mrel @ Q @ R) | (mrel @ R @ (sk14 @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | ~ (mrel @ P @ Q) | (mrel @ Q @ (sk15 @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (mrel @ O @ P) | (mrel @ P @ (sk16 @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | (mrel @ O @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | (v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | (mrel @ O @ (sk18 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (mrel @ N @ O) | ~ (v13 @ (sk18 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | (mrel @ N @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | (v14 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | (mrel @ N @ (sk20 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (mrel @ M @ N) | ~ (v14 @ (sk20 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | (mrel @ M @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | (v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | (mrel @ M @ (sk22 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (mrel @ L @ M) | ~ (v15 @ (sk22 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | (mrel @ L @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | (v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | (mrel @ L @ (sk24 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | ~ (mrel @ K @ L) | ~ (v16 @ (sk24 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | ~ (mrel @ J @ K) | (mrel @ K @ (sk25 @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | ~ (mrel @ I @ J) | (mrel @ J @ (sk26 @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | ~ (mrel @ H @ I) | (mrel @ I @ (sk27 @ I @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (mrel @ G @ H) | (mrel @ H @ (sk28 @ H @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | (mrel @ G @ (sk29 @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | (v21 @ (sk29 @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | (mrel @ G @ (sk30 @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (mrel @ F @ G) | ~ (v21 @ (sk30 @ G @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | (mrel @ F @ (sk31 @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | (v22 @ (sk31 @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | (mrel @ F @ (sk32 @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (mrel @ E @ F) | ~ (v22 @ (sk32 @ F @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | (mrel @ E @ (sk33 @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | (v23 @ (sk33 @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | (mrel @ E @ (sk34 @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (mrel @ D @ E) | ~ (v23 @ (sk34 @ E @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | (mrel @ D @ (sk35 @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | (v24 @ (sk35 @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | (mrel @ D @ (sk36 @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | ~ (mrel @ C @ D) | ~ (v24 @ (sk36 @ D @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | ~ (mrel @ B @ C) | (mrel @ C @ (sk37 @ C @ B @ A))) & (~ (mrel @ mactual @ A) | ~ (mrel @ A @ B) | (mrel @ B @ (sk38 @ B @ A))) & (~ (mrel @ mactual @ A) | (mrel @ A @ (sk39 @ A))) & (mrel @ mactual @ sk40)))),inference(cnf,[status(esa)],[104])).
% 88.18/39.56  thf(128,plain,(! [M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(3,axiom,((! [A:mworld,B:mworld]: (mrel @ A @ B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_universal)).
% 88.18/39.56  thf(56,plain,((! [A:mworld,B:mworld]: (mrel @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 88.18/39.56  thf(57,plain,(! [B:mworld,A:mworld] : ((mrel @ A @ B))),inference(cnf,[status(esa)],[56])).
% 88.18/39.56  thf(11393,plain,(! [M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[128,57])).
% 88.18/39.56  thf(11394,plain,(! [M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[11393])).
% 88.18/39.56  thf(42,axiom,((mlocal @ (mbox @ (mor @ v28 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mor @ v14 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v9))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod4)).
% 88.18/39.56  thf(198,plain,((! [A:mworld]: ((mrel @ mactual @ A) => ((v28 @ A) | ! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (~ (v15 @ N) | ! [O:mworld]: ((mrel @ N @ O) => ((v14 @ O) | ! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (v9 @ T)))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 88.18/39.56  thf(199,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (v28 @ A) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (v15 @ N)) | (~ (mrel @ N @ O)) | (v14 @ O) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (v9 @ T))),inference(cnf,[status(esa)],[198])).
% 88.18/39.56  thf(163,plain,(! [V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(18992,plain,(! [V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[163,57])).
% 88.18/39.56  thf(18993,plain,(! [V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[18992])).
% 88.18/39.56  thf(123,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(10838,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[123,57])).
% 88.18/39.56  thf(10839,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[10838])).
% 88.18/39.56  thf(108,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(6676,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[108,57])).
% 88.18/39.56  thf(6677,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[6676])).
% 88.18/39.56  thf(6,axiom,((mlocal @ (mbox @ (mor @ (mnot @ v28) @ (mbox @ (mbox @ (mor @ v26 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v16) @ (mbox @ (mbox @ (mbox @ (mnot @ v13)))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod6)).
% 88.18/39.56  thf(62,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (~ (v28 @ A) | ! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => ((v26 @ C) | ! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (~ (v16 @ M) | ! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (~ (v13 @ P))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 88.18/39.56  thf(63,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (v28 @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (v26 @ C) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (v16 @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (v13 @ P)))),inference(cnf,[status(esa)],[62])).
% 88.18/39.56  thf(294,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | (~ (v28 @ A)) | ~ (($true)) | ~ (($true)) | (v26 @ B) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v16 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v13 @ D)))),inference(rewrite,[status(thm)],[63,57])).
% 88.18/39.56  thf(295,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (v26 @ B) | (~ (v16 @ C)) | (~ (v13 @ D)))),inference(simp,[status(thm)],[294])).
% 88.18/39.56  thf(160,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (v24 @ (sk35 @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(235,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v24 @ (sk35 @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[160,57])).
% 88.18/39.56  thf(236,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v24 @ (sk35 @ D @ C @ B @ A)))),inference(simp,[status(thm)],[235])).
% 88.18/39.56  thf(5,axiom,((mlocal @ (mbox @ (mor @ (mnot @ v28) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mor @ v22 @ (mbox @ (mbox @ (mbox @ (mbox @ v18)))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod8)).
% 88.18/39.56  thf(60,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (~ (v28 @ A) | ! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (~ (v24 @ E) | ! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => ((v22 @ G) | ! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (v18 @ K)))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 88.18/39.56  thf(61,plain,(! [K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (v28 @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (v24 @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (v22 @ G) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (v18 @ K))),inference(cnf,[status(esa)],[60])).
% 88.18/39.56  thf(264,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | (~ (v28 @ A)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v24 @ B)) | ~ (($true)) | ~ (($true)) | (v22 @ C) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v18 @ D))),inference(rewrite,[status(thm)],[61,57])).
% 88.18/39.56  thf(265,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v24 @ B)) | (v22 @ C) | (v18 @ D))),inference(simp,[status(thm)],[264])).
% 88.18/39.56  thf(139,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (v22 @ (sk32 @ F @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(251,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v22 @ (sk32 @ F @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[139,57])).
% 88.18/39.56  thf(252,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v22 @ (sk32 @ F @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[251])).
% 88.18/39.56  thf(266,plain,(! [J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v24 @ B)) | (v18 @ D) | ~ (($true)) | ((v22 @ C) != (v22 @ (sk32 @ J @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[265,252])).
% 88.18/39.56  thf(267,plain,(! [J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v24 @ B)) | (v18 @ D) | ((v22 @ C) != (v22 @ (sk32 @ J @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[266])).
% 88.18/39.56  thf(268,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v24 @ B)) | (v18 @ C))),inference(pattern_uni,[status(thm)],[267:[bind(A, $thf(:)),bind(B, $thf(>)),bind(C, $thf(sk32 @ K @ L @ M @ N @ O @ P)),bind(D, $thf(D)),bind(E, $thf(P)),bind(F, $thf(O)),bind(G, $thf(N)),bind(H, $thf(M)),bind(I, $thf(L)),bind(J, $thf(K))]])).
% 88.18/39.56  thf(276,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v24 @ B)) | (v18 @ C))),inference(simp,[status(thm)],[268])).
% 88.18/39.56  thf(278,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ E)) | ~ (($true)) | (v18 @ G) | ((v24 @ (sk35 @ D @ C @ B @ A)) != (v24 @ F)))),inference(paramod_ordered,[status(thm)],[236,276])).
% 88.18/39.56  thf(279,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ E)) | (v18 @ G) | ((v24 @ (sk35 @ D @ C @ B @ A)) != (v24 @ F)))),inference(simp,[status(thm)],[278])).
% 88.18/39.56  thf(280,plain,(! [B:mworld,A:mworld] : ((~ (v28 @ A)) | (v18 @ B))),inference(pattern_uni,[status(thm)],[279:[bind(A, $thf(K)),bind(B, $thf(J)),bind(C, $thf(I)),bind(D, $thf(H)),bind(E, $thf(E)),bind(F, $thf(sk35 @ H @ I @ J @ K))]])).
% 88.18/39.56  thf(284,plain,(! [B:mworld,A:mworld] : ((~ (v28 @ A)) | (v18 @ B))),inference(simp,[status(thm)],[280])).
% 88.18/39.56  thf(23,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v26) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v18) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v6))))))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod23)).
% 88.18/39.56  thf(96,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (~ (v26 @ C) | ! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (~ (v18 @ K) | ! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (~ (v15 @ N) | ! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (~ (v6 @ W))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 88.18/39.56  thf(97,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (v26 @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (v18 @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (v15 @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (v6 @ W)))),inference(cnf,[status(esa)],[96])).
% 88.18/39.56  thf(345,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v26 @ A)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v18 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v15 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v6 @ D)))),inference(rewrite,[status(thm)],[97,57])).
% 88.18/39.56  thf(346,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (~ (v18 @ B)) | (~ (v15 @ C)) | (~ (v6 @ D)))),inference(simp,[status(thm)],[345])).
% 88.18/39.56  thf(356,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v26 @ C)) | ~ (($true)) | (~ (v15 @ E)) | (~ (v6 @ F)) | ((v18 @ B) != (v18 @ D)))),inference(paramod_ordered,[status(thm)],[284,346])).
% 88.18/39.56  thf(357,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v26 @ C)) | (~ (v15 @ E)) | (~ (v6 @ F)) | ((v18 @ B) != (v18 @ D)))),inference(simp,[status(thm)],[356])).
% 88.18/39.56  thf(358,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v26 @ B)) | (~ (v15 @ C)) | (~ (v6 @ D)))),inference(pattern_uni,[status(thm)],[357:[bind(A, $thf(.)),bind(B, $thf(/)),bind(C, $thf(2)),bind(D, $thf(/))]])).
% 88.18/39.56  thf(367,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v26 @ B)) | (~ (v15 @ C)) | (~ (v6 @ D)))),inference(simp,[status(thm)],[358])).
% 88.18/39.56  thf(383,plain,(! [H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v16 @ C)) | (~ (v13 @ D)) | (~ (v28 @ E)) | ~ (($true)) | (~ (v15 @ G)) | (~ (v6 @ H)) | ((v26 @ B) != (v26 @ F)))),inference(paramod_ordered,[status(thm)],[295,367])).
% 88.18/39.56  thf(384,plain,(! [H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v16 @ C)) | (~ (v13 @ D)) | (~ (v28 @ E)) | (~ (v15 @ G)) | (~ (v6 @ H)) | ((v26 @ B) != (v26 @ F)))),inference(simp,[status(thm)],[383])).
% 88.18/39.56  thf(385,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v16 @ B)) | (~ (v13 @ C)) | (~ (v28 @ D)) | (~ (v15 @ E)) | (~ (v6 @ F)))),inference(pattern_uni,[status(thm)],[384:[bind(A, $thf(5)),bind(B, $thf(7)),bind(C, $thf(A)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(7))]])).
% 88.18/39.56  thf(386,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v16 @ B)) | (~ (v13 @ C)) | (~ (v28 @ D)) | (~ (v15 @ E)) | (~ (v6 @ F)))),inference(simp,[status(thm)],[385])).
% 88.18/39.56  thf(659,plain,(! [F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v16 @ B)) | (~ (v13 @ C)) | (~ (v15 @ E)) | (~ (v6 @ F)) | ((v28 @ D) != (v28 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[386])).
% 88.18/39.56  thf(660,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ C)) | (~ (v16 @ A)) | (~ (v13 @ B)) | (~ (v15 @ D)) | (~ (v6 @ E)))),inference(pattern_uni,[status(thm)],[659:[bind(A, $thf(D))]])).
% 88.18/39.56  thf(664,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ C)) | (~ (v16 @ A)) | (~ (v13 @ B)) | (~ (v15 @ D)) | (~ (v6 @ E)))),inference(simp,[status(thm)],[660])).
% 88.18/39.56  thf(6720,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ R)) | (~ (v16 @ P)) | ~ (($true)) | (~ (v15 @ S)) | (~ (v6 @ T)) | ((v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v13 @ Q)))),inference(paramod_ordered,[status(thm)],[6677,664])).
% 88.18/39.56  thf(6721,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ R)) | (~ (v16 @ P)) | (~ (v15 @ S)) | (~ (v6 @ T)) | ((v13 @ (sk17 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v13 @ Q)))),inference(simp,[status(thm)],[6720])).
% 88.18/39.56  thf(6722,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ B)) | (~ (v16 @ A)) | (~ (v15 @ C)) | (~ (v6 @ D)))),inference(pattern_uni,[status(thm)],[6721:[bind(A, $thf(ZI)),bind(B, $thf(ZH)),bind(C, $thf(ZG)),bind(D, $thf(ZF)),bind(E, $thf(ZE)),bind(F, $thf(ZD)),bind(G, $thf(ZC)),bind(H, $thf(ZB)),bind(I, $thf(ZA)),bind(J, $thf(Z)),bind(K, $thf(Y)),bind(L, $thf(X)),bind(M, $thf(W)),bind(N, $thf(V)),bind(O, $thf(U)),bind(P, $thf(P)),bind(Q, $thf(sk17 @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI))]])).
% 88.18/39.56  thf(6730,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ B)) | (~ (v16 @ A)) | (~ (v15 @ C)) | (~ (v6 @ D)))),inference(simp,[status(thm)],[6722])).
% 88.18/39.56  thf(10857,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ N)) | ~ (($true)) | (~ (v15 @ O)) | (~ (v6 @ P)) | ((v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v16 @ M)))),inference(paramod_ordered,[status(thm)],[10839,6730])).
% 88.18/39.56  thf(10858,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ N)) | (~ (v15 @ O)) | (~ (v6 @ P)) | ((v16 @ (sk23 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v16 @ M)))),inference(simp,[status(thm)],[10857])).
% 88.18/39.56  thf(10859,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v15 @ B)) | (~ (v6 @ C)))),inference(pattern_uni,[status(thm)],[10858:[bind(A, $thf(ZB)),bind(B, $thf(ZA)),bind(C, $thf(Z)),bind(D, $thf(Y)),bind(E, $thf(X)),bind(F, $thf(W)),bind(G, $thf(V)),bind(H, $thf(U)),bind(I, $thf(T)),bind(J, $thf(S)),bind(K, $thf(R)),bind(L, $thf(Q)),bind(M, $thf(sk23 @ Q @ R @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB))]])).
% 88.18/39.56  thf(10876,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v15 @ B)) | (~ (v6 @ C)))),inference(simp,[status(thm)],[10859])).
% 88.18/39.56  thf(11398,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ N)) | ~ (($true)) | (~ (v6 @ P)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ O)))),inference(paramod_ordered,[status(thm)],[11394,10876])).
% 88.18/39.56  thf(11399,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ N)) | (~ (v6 @ P)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ O)))),inference(simp,[status(thm)],[11398])).
% 88.18/39.56  thf(11400,plain,(! [B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v6 @ B)))),inference(pattern_uni,[status(thm)],[11399:[bind(A, $thf(ZC)),bind(B, $thf(ZB)),bind(C, $thf(ZA)),bind(D, $thf(Z)),bind(E, $thf(Y)),bind(F, $thf(X)),bind(G, $thf(W)),bind(H, $thf(V)),bind(I, $thf(U)),bind(J, $thf(T)),bind(K, $thf(S)),bind(L, $thf(R)),bind(M, $thf(Q)),bind(N, $thf(N)),bind(O, $thf(sk21 @ Q @ R @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC))]])).
% 88.18/39.56  thf(11458,plain,(! [B:mworld,A:mworld] : ((~ (v28 @ A)) | (~ (v6 @ B)))),inference(simp,[status(thm)],[11400])).
% 88.18/39.56  thf(18997,plain,(! [X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ W)) | ~ (($true)) | ((v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v6 @ X)))),inference(paramod_ordered,[status(thm)],[18993,11458])).
% 88.18/39.56  thf(18998,plain,(! [X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v28 @ W)) | ((v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v6 @ X)))),inference(simp,[status(thm)],[18997])).
% 88.18/39.56  thf(18999,plain,(! [A:mworld] : ((~ (v28 @ A)))),inference(pattern_uni,[status(thm)],[18998:[bind(A, $thf(ZT)),bind(B, $thf(ZS)),bind(C, $thf(ZR)),bind(D, $thf(ZQ)),bind(E, $thf(ZP)),bind(F, $thf(ZO)),bind(G, $thf(ZN)),bind(H, $thf(ZM)),bind(I, $thf(ZL)),bind(J, $thf(ZK)),bind(K, $thf(ZJ)),bind(L, $thf(ZI)),bind(M, $thf(ZH)),bind(N, $thf(ZG)),bind(O, $thf(ZF)),bind(P, $thf(ZE)),bind(Q, $thf(ZD)),bind(R, $thf(ZC)),bind(S, $thf(ZB)),bind(T, $thf(ZA)),bind(U, $thf(Z)),bind(V, $thf(Y)),bind(W, $thf(W)),bind(X, $thf(sk7 @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT))]])).
% 88.18/39.56  thf(19044,plain,(! [A:mworld] : ((~ (v28 @ A)))),inference(simp,[status(thm)],[18999])).
% 88.18/39.56  thf(7,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v13 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v5 @ (mbox @ (mbox @ (mor @ v3 @ (mbox @ v2)))))))))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod47)).
% 88.18/39.56  thf(64,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => ((v13 @ P) | ! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (! [X:mworld]: ((mrel @ W @ X) => ((v5 @ X) | ! [Y:mworld]: ((mrel @ X @ Y) => (! [Z:mworld]: ((mrel @ Y @ Z) => ((v3 @ Z) | ! [ZA:mworld]: ((mrel @ Z @ ZA) => (v2 @ ZA)))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 88.18/39.56  thf(65,plain,(! [ZA:mworld,Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (v13 @ P) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (mrel @ W @ X)) | (v5 @ X) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (v3 @ Z) | (~ (mrel @ Z @ ZA)) | (v2 @ ZA))),inference(cnf,[status(esa)],[64])).
% 88.18/39.56  thf(331,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v13 @ A) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v5 @ B) | ~ (($true)) | ~ (($true)) | (v3 @ C) | ~ (($true)) | (v2 @ D))),inference(rewrite,[status(thm)],[65,57])).
% 88.18/39.56  thf(332,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v13 @ A) | (v5 @ B) | (v3 @ C) | (v2 @ D))),inference(simp,[status(thm)],[331])).
% 88.18/39.56  thf(120,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (v13 @ (sk18 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(321,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v13 @ (sk18 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[120,57])).
% 88.18/39.56  thf(322,plain,(! [O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v13 @ (sk18 @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[321])).
% 88.18/39.56  thf(339,plain,(! [S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v5 @ B) | (v3 @ C) | (v2 @ D) | ~ (($true)) | ((v13 @ A) != (v13 @ (sk18 @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[332,322])).
% 88.18/39.56  thf(340,plain,(! [S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v5 @ B) | (v3 @ C) | (v2 @ D) | ((v13 @ A) != (v13 @ (sk18 @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[339])).
% 88.18/39.56  thf(341,plain,(! [C:mworld,B:mworld,A:mworld] : ((v5 @ A) | (v3 @ B) | (v2 @ C))),inference(pattern_uni,[status(thm)],[340:[bind(A, $thf(sk18 @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH)),bind(B, $thf(A)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(ZH)),bind(F, $thf(ZG)),bind(G, $thf(ZF)),bind(H, $thf(ZE)),bind(I, $thf(ZD)),bind(J, $thf(ZC)),bind(K, $thf(ZB)),bind(L, $thf(ZA)),bind(M, $thf(Z)),bind(N, $thf(Y)),bind(O, $thf(X)),bind(P, $thf(W)),bind(Q, $thf(V)),bind(R, $thf(U)),bind(S, $thf(T))]])).
% 88.18/39.56  thf(343,plain,(! [C:mworld,B:mworld,A:mworld] : ((v5 @ A) | (v3 @ B) | (v2 @ C))),inference(simp,[status(thm)],[341])).
% 88.18/39.56  thf(155,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (v5 @ (sk6 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(18741,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v5 @ (sk6 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[155,57])).
% 88.18/39.56  thf(18742,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v5 @ (sk6 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[18741])).
% 88.18/39.56  thf(18764,plain,(! [Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v3 @ B) | (v2 @ C) | ~ (($true)) | ((v5 @ A) != (v5 @ (sk6 @ Z @ Y @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D))))),inference(paramod_ordered,[status(thm)],[343,18742])).
% 88.18/39.56  thf(18765,plain,(! [Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v3 @ B) | (v2 @ C) | ((v5 @ A) != (v5 @ (sk6 @ Z @ Y @ X @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D))))),inference(simp,[status(thm)],[18764])).
% 88.18/39.56  thf(18766,plain,(! [B:mworld,A:mworld] : ((v3 @ A) | (v2 @ B))),inference(pattern_uni,[status(thm)],[18765:[bind(A, $thf(sk6 @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU @ ZV @ ZW)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(ZW)),bind(E, $thf(ZV)),bind(F, $thf(ZU)),bind(G, $thf(ZT)),bind(H, $thf(ZS)),bind(I, $thf(ZR)),bind(J, $thf(ZQ)),bind(K, $thf(ZP)),bind(L, $thf(ZO)),bind(M, $thf(ZN)),bind(N, $thf(ZM)),bind(O, $thf(ZL)),bind(P, $thf(ZK)),bind(Q, $thf(ZJ)),bind(R, $thf(ZI)),bind(S, $thf(ZH)),bind(T, $thf(ZG)),bind(U, $thf(ZF)),bind(V, $thf(ZE)),bind(W, $thf(ZD)),bind(X, $thf(ZC)),bind(Y, $thf(ZB)),bind(Z, $thf(ZA))]])).
% 88.18/39.56  thf(18796,plain,(! [B:mworld,A:mworld] : ((v3 @ A) | (v2 @ B))),inference(simp,[status(thm)],[18766])).
% 88.18/39.56  thf(18,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v16 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v9) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v6) @ (mbox @ (mbox @ (mbox @ (mnot @ v3)))))))))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod45)).
% 88.18/39.56  thf(86,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => ((v16 @ M) | ! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (~ (v9 @ T) | ! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (~ (v6 @ W) | ! [X:mworld]: ((mrel @ W @ X) => (! [Y:mworld]: ((mrel @ X @ Y) => (! [Z:mworld]: ((mrel @ Y @ Z) => (~ (v3 @ Z))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 88.18/39.56  thf(87,plain,(! [Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (v16 @ M) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (v9 @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (v6 @ W)) | (~ (mrel @ W @ X)) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (~ (v3 @ Z)))),inference(cnf,[status(esa)],[86])).
% 88.18/39.56  thf(2454,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v16 @ A) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v9 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v6 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v3 @ D)))),inference(rewrite,[status(thm)],[87,57])).
% 88.18/39.56  thf(2455,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v16 @ A) | (~ (v9 @ B)) | (~ (v6 @ C)) | (~ (v3 @ D)))),inference(simp,[status(thm)],[2454])).
% 88.18/39.56  thf(162,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (v16 @ (sk24 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(290,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v16 @ (sk24 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[162,57])).
% 88.18/39.56  thf(291,plain,(! [L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v16 @ (sk24 @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[290])).
% 88.18/39.56  thf(2495,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ B)) | (~ (v6 @ C)) | (~ (v3 @ D)) | ~ (($true)) | ((v16 @ A) != (v16 @ (sk24 @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[2455,291])).
% 88.18/39.56  thf(2496,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ B)) | (~ (v6 @ C)) | (~ (v3 @ D)) | ((v16 @ A) != (v16 @ (sk24 @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[2495])).
% 88.18/39.56  thf(2497,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v6 @ B)) | (~ (v3 @ C)))),inference(pattern_uni,[status(thm)],[2496:[bind(A, $thf(sk24 @ Q @ R @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB)),bind(B, $thf(>)),bind(C, $thf(A)),bind(D, $thf(D)),bind(E, $thf(ZB)),bind(F, $thf(ZA)),bind(G, $thf(Z)),bind(H, $thf(Y)),bind(I, $thf(X)),bind(J, $thf(W)),bind(K, $thf(V)),bind(L, $thf(U)),bind(M, $thf(T)),bind(N, $thf(S)),bind(O, $thf(R)),bind(P, $thf(Q))]])).
% 88.18/39.56  thf(2517,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v6 @ B)) | (~ (v3 @ C)))),inference(simp,[status(thm)],[2497])).
% 88.18/39.56  thf(19020,plain,(! [Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ W)) | ~ (($true)) | (~ (v3 @ Y)) | ((v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v6 @ X)))),inference(paramod_ordered,[status(thm)],[18993,2517])).
% 88.18/39.56  thf(19021,plain,(! [Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ W)) | (~ (v3 @ Y)) | ((v6 @ (sk7 @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v6 @ X)))),inference(simp,[status(thm)],[19020])).
% 88.18/39.56  thf(19022,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v3 @ B)))),inference(pattern_uni,[status(thm)],[19021:[bind(A, $thf(ZU)),bind(B, $thf(ZT)),bind(C, $thf(ZS)),bind(D, $thf(ZR)),bind(E, $thf(ZQ)),bind(F, $thf(ZP)),bind(G, $thf(ZO)),bind(H, $thf(ZN)),bind(I, $thf(ZM)),bind(J, $thf(ZL)),bind(K, $thf(ZK)),bind(L, $thf(ZJ)),bind(M, $thf(ZI)),bind(N, $thf(ZH)),bind(O, $thf(ZG)),bind(P, $thf(ZF)),bind(Q, $thf(ZE)),bind(R, $thf(ZD)),bind(S, $thf(ZC)),bind(T, $thf(ZB)),bind(U, $thf(ZA)),bind(V, $thf(Z)),bind(W, $thf(W)),bind(X, $thf(sk7 @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU))]])).
% 88.18/39.56  thf(19040,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v3 @ B)))),inference(simp,[status(thm)],[19022])).
% 88.18/39.56  thf(19058,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v2 @ B) | (~ (v9 @ C)) | ~ (($true)) | ((v3 @ A) != (v3 @ D)))),inference(paramod_ordered,[status(thm)],[18796,19040])).
% 88.18/39.56  thf(19059,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v2 @ B) | (~ (v9 @ C)) | ((v3 @ A) != (v3 @ D)))),inference(simp,[status(thm)],[19058])).
% 88.18/39.56  thf(19060,plain,(! [B:mworld,A:mworld] : ((v2 @ A) | (~ (v9 @ B)))),inference(pattern_uni,[status(thm)],[19059:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(A))]])).
% 88.18/39.56  thf(19075,plain,(! [B:mworld,A:mworld] : ((v2 @ A) | (~ (v9 @ B)))),inference(simp,[status(thm)],[19060])).
% 88.18/39.56  thf(166,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(19260,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[166,57])).
% 88.18/39.56  thf(19261,plain,(! [W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[19260])).
% 88.18/39.56  thf(137,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(14215,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[137,57])).
% 88.18/39.56  thf(14216,plain,(! [T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[14215])).
% 88.18/39.56  thf(13,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v9) @ (mbox @ (mor @ (mnot @ v8) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v5) @ (mbox @ (mbox @ (mbox @ (mbox @ v1))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod49)).
% 88.18/39.56  thf(76,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => (! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (~ (v9 @ T) | ! [U:mworld]: ((mrel @ T @ U) => (~ (v8 @ U) | ! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (! [X:mworld]: ((mrel @ W @ X) => (~ (v5 @ X) | ! [Y:mworld]: ((mrel @ X @ Y) => (! [Z:mworld]: ((mrel @ Y @ Z) => (! [ZA:mworld]: ((mrel @ Z @ ZA) => (! [ZB:mworld]: ((mrel @ ZA @ ZB) => (v1 @ ZB)))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 88.18/39.56  thf(77,plain,(! [ZB:mworld,ZA:mworld,Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (v9 @ T)) | (~ (mrel @ T @ U)) | (~ (v8 @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (mrel @ W @ X)) | (~ (v5 @ X)) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (~ (mrel @ Z @ ZA)) | (~ (mrel @ ZA @ ZB)) | (v1 @ ZB))),inference(cnf,[status(esa)],[76])).
% 88.18/39.56  thf(831,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v9 @ A)) | ~ (($true)) | (~ (v8 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v5 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v1 @ D))),inference(rewrite,[status(thm)],[77,57])).
% 88.18/39.56  thf(832,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (v1 @ D))),inference(simp,[status(thm)],[831])).
% 88.18/39.56  thf(20,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v2) @ (mbox @ (mnot @ v1)))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mod34)).
% 88.18/39.56  thf(90,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (! [E:mworld]: ((mrel @ D @ E) => (! [F:mworld]: ((mrel @ E @ F) => ((v23 @ F) | ! [G:mworld]: ((mrel @ F @ G) => (! [H:mworld]: ((mrel @ G @ H) => (! [I:mworld]: ((mrel @ H @ I) => (! [J:mworld]: ((mrel @ I @ J) => (! [K:mworld]: ((mrel @ J @ K) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (~ (v15 @ N) | ! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (! [W:mworld]: ((mrel @ V @ W) => (! [X:mworld]: ((mrel @ W @ X) => (! [Y:mworld]: ((mrel @ X @ Y) => (! [Z:mworld]: ((mrel @ Y @ Z) => (! [ZA:mworld]: ((mrel @ Z @ ZA) => (~ (v2 @ ZA) | ! [ZB:mworld]: ((mrel @ ZA @ ZB) => (~ (v1 @ ZB))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 88.18/39.56  thf(91,plain,(! [ZB:mworld,ZA:mworld,Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (v23 @ F) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (v15 @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (mrel @ W @ X)) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (~ (mrel @ Z @ ZA)) | (~ (v2 @ ZA)) | (~ (mrel @ ZA @ ZB)) | (~ (v1 @ ZB)))),inference(cnf,[status(esa)],[90])).
% 88.18/39.56  thf(3292,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v23 @ A) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v15 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v2 @ C)) | ~ (($true)) | (~ (v1 @ D)))),inference(rewrite,[status(thm)],[91,57])).
% 88.18/39.56  thf(3293,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v23 @ A) | (~ (v15 @ B)) | (~ (v2 @ C)) | (~ (v1 @ D)))),inference(simp,[status(thm)],[3292])).
% 88.18/39.56  thf(144,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (v23 @ (sk34 @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(231,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v23 @ (sk34 @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[144,57])).
% 88.18/39.56  thf(232,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v23 @ (sk34 @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[231])).
% 88.18/39.56  thf(3342,plain,(! [I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v15 @ B)) | (~ (v2 @ C)) | (~ (v1 @ D)) | ~ (($true)) | ((v23 @ A) != (v23 @ (sk34 @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[3293,232])).
% 88.18/39.56  thf(3343,plain,(! [I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v15 @ B)) | (~ (v2 @ C)) | (~ (v1 @ D)) | ((v23 @ A) != (v23 @ (sk34 @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[3342])).
% 88.18/39.56  thf(3344,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v15 @ A)) | (~ (v2 @ B)) | (~ (v1 @ C)))),inference(pattern_uni,[status(thm)],[3343:[bind(A, $thf(sk34 @ J @ K @ L @ M @ N)),bind(B, $thf(6)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(N)),bind(F, $thf(M)),bind(G, $thf(L)),bind(H, $thf(K)),bind(I, $thf(J))]])).
% 88.18/39.56  thf(3356,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v15 @ A)) | (~ (v2 @ B)) | (~ (v1 @ C)))),inference(simp,[status(thm)],[3344])).
% 88.18/39.56  thf(3401,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v15 @ E)) | (~ (v2 @ F)) | ~ (($true)) | ((v1 @ D) != (v1 @ G)))),inference(paramod_ordered,[status(thm)],[832,3356])).
% 88.18/39.56  thf(3402,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v15 @ E)) | (~ (v2 @ F)) | ((v1 @ D) != (v1 @ G)))),inference(simp,[status(thm)],[3401])).
% 88.18/39.56  thf(3403,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v15 @ D)) | (~ (v2 @ E)))),inference(pattern_uni,[status(thm)],[3402:[bind(A, $thf(<)),bind(B, $thf(=)),bind(C, $thf(@)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(D))]])).
% 88.18/39.56  thf(3416,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v15 @ D)) | (~ (v2 @ E)))),inference(simp,[status(thm)],[3403])).
% 88.18/39.56  thf(11433,plain,(! [R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ N)) | (~ (v8 @ O)) | (~ (v5 @ P)) | ~ (($true)) | (~ (v2 @ R)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ Q)))),inference(paramod_ordered,[status(thm)],[11394,3416])).
% 88.18/39.56  thf(11434,plain,(! [R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ N)) | (~ (v8 @ O)) | (~ (v5 @ P)) | (~ (v2 @ R)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ Q)))),inference(simp,[status(thm)],[11433])).
% 88.18/39.56  thf(11435,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v2 @ D)))),inference(pattern_uni,[status(thm)],[11434:[bind(A, $thf(ZE)),bind(B, $thf(ZD)),bind(C, $thf(ZC)),bind(D, $thf(ZB)),bind(E, $thf(ZA)),bind(F, $thf(Z)),bind(G, $thf(Y)),bind(H, $thf(X)),bind(I, $thf(W)),bind(J, $thf(V)),bind(K, $thf(U)),bind(L, $thf(T)),bind(M, $thf(S)),bind(N, $thf(N)),bind(O, $thf(O)),bind(P, $thf(P)),bind(Q, $thf(sk21 @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE))]])).
% 88.18/39.56  thf(11461,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v2 @ D)))),inference(simp,[status(thm)],[11435])).
% 88.18/39.56  thf(14238,plain,(! [X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ U)) | ~ (($true)) | (~ (v5 @ W)) | (~ (v2 @ X)) | ((v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v8 @ V)))),inference(paramod_ordered,[status(thm)],[14216,11461])).
% 88.18/39.56  thf(14239,plain,(! [X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ U)) | (~ (v5 @ W)) | (~ (v2 @ X)) | ((v8 @ (sk11 @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v8 @ V)))),inference(simp,[status(thm)],[14238])).
% 88.18/39.56  thf(14240,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v5 @ B)) | (~ (v2 @ C)))),inference(pattern_uni,[status(thm)],[14239:[bind(A, $thf(ZR)),bind(B, $thf(ZQ)),bind(C, $thf(ZP)),bind(D, $thf(ZO)),bind(E, $thf(ZN)),bind(F, $thf(ZM)),bind(G, $thf(ZL)),bind(H, $thf(ZK)),bind(I, $thf(ZJ)),bind(J, $thf(ZI)),bind(K, $thf(ZH)),bind(L, $thf(ZG)),bind(M, $thf(ZF)),bind(N, $thf(ZE)),bind(O, $thf(ZD)),bind(P, $thf(ZC)),bind(Q, $thf(ZB)),bind(R, $thf(ZA)),bind(S, $thf(Z)),bind(T, $thf(Y)),bind(U, $thf(U)),bind(V, $thf(sk11 @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR))]])).
% 88.18/39.56  thf(14250,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v5 @ B)) | (~ (v2 @ C)))),inference(simp,[status(thm)],[14240])).
% 88.18/39.56  thf(19270,plain,(! [Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ X)) | ~ (($true)) | (~ (v2 @ Z)) | ((v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v5 @ Y)))),inference(paramod_ordered,[status(thm)],[19261,14250])).
% 88.18/39.56  thf(19271,plain,(! [Z:mworld,Y:mworld,X:mworld,W:mworld,V:mworld,U:mworld,T:mworld,S:mworld,R:mworld,Q:mworld,P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ X)) | (~ (v2 @ Z)) | ((v5 @ (sk5 @ W @ V @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v5 @ Y)))),inference(simp,[status(thm)],[19270])).
% 88.18/39.56  thf(19272,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v2 @ B)))),inference(pattern_uni,[status(thm)],[19271:[bind(A, $thf(ZW)),bind(B, $thf(ZV)),bind(C, $thf(ZU)),bind(D, $thf(ZT)),bind(E, $thf(ZS)),bind(F, $thf(ZR)),bind(G, $thf(ZQ)),bind(H, $thf(ZP)),bind(I, $thf(ZO)),bind(J, $thf(ZN)),bind(K, $thf(ZM)),bind(L, $thf(ZL)),bind(M, $thf(ZK)),bind(N, $thf(ZJ)),bind(O, $thf(ZI)),bind(P, $thf(ZH)),bind(Q, $thf(ZG)),bind(R, $thf(ZF)),bind(S, $thf(ZE)),bind(T, $thf(ZD)),bind(U, $thf(ZC)),bind(V, $thf(ZB)),bind(W, $thf(ZA)),bind(X, $thf(X)),bind(Y, $thf(sk5 @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU @ ZV @ ZW))]])).
% 88.18/39.56  thf(19279,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v2 @ B)))),inference(simp,[status(thm)],[19272])).
% 88.18/39.56  thf(19292,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ B)) | (~ (v9 @ C)) | ~ (($true)) | ((v2 @ A) != (v2 @ D)))),inference(paramod_ordered,[status(thm)],[19075,19279])).
% 88.18/39.56  thf(19293,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v9 @ B)) | (~ (v9 @ C)) | ((v2 @ A) != (v2 @ D)))),inference(simp,[status(thm)],[19292])).
% 88.18/39.56  thf(19294,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v9 @ B)))),inference(pattern_uni,[status(thm)],[19293:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(A))]])).
% 88.18/39.56  thf(19312,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | (~ (v9 @ B)))),inference(simp,[status(thm)],[19294])).
% 88.18/39.56  thf(19319,plain,(! [B:mworld,A:mworld] : ((~ (v9 @ A)) | ((v9 @ B) != (v9 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[19312])).
% 88.18/39.56  thf(19320,plain,(! [A:mworld] : ((~ (v9 @ A)))),inference(pattern_uni,[status(thm)],[19319:[bind(A, $thf(B))]])).
% 88.18/39.56  thf(19323,plain,(! [A:mworld] : ((~ (v9 @ A)))),inference(simp,[status(thm)],[19320])).
% 88.18/39.56  thf(19674,plain,(! [B:mworld,A:mworld] : (~ (($true)) | ($false) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v15 @ A)) | ~ (($true)) | (v14 @ B) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ($false))),inference(rewrite,[status(thm)],[199,19044,57,19323])).
% 88.18/39.56  thf(19675,plain,(! [B:mworld,A:mworld] : ((~ (v15 @ A)) | (v14 @ B))),inference(simp,[status(thm)],[19674])).
% 88.18/39.56  thf(134,plain,(! [N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (mrel @ mactual @ A)) | (~ (mrel @ A @ B)) | (~ (mrel @ B @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (~ (mrel @ G @ H)) | (~ (mrel @ H @ I)) | (~ (mrel @ I @ J)) | (~ (mrel @ J @ K)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (v14 @ (sk20 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[105])).
% 88.18/39.56  thf(307,plain,(! [N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v14 @ (sk20 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(rewrite,[status(thm)],[134,57])).
% 88.18/39.56  thf(308,plain,(! [N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v14 @ (sk20 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A))))),inference(simp,[status(thm)],[307])).
% 88.18/39.56  thf(19679,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v15 @ A)) | ~ (($true)) | ((v14 @ B) != (v14 @ (sk20 @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C))))),inference(paramod_ordered,[status(thm)],[19675,308])).
% 88.18/39.56  thf(19680,plain,(! [P:mworld,O:mworld,N:mworld,M:mworld,L:mworld,K:mworld,J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v15 @ A)) | ((v14 @ B) != (v14 @ (sk20 @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C))))),inference(simp,[status(thm)],[19679])).
% 88.18/39.56  thf(19681,plain,(! [A:mworld] : ((~ (v15 @ A)))),inference(pattern_uni,[status(thm)],[19680:[bind(A, $thf(A)),bind(B, $thf(sk20 @ Q @ R @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD)),bind(C, $thf(ZD)),bind(D, $thf(ZC)),bind(E, $thf(ZB)),bind(F, $thf(ZA)),bind(G, $thf(Z)),bind(H, $thf(Y)),bind(I, $thf(X)),bind(J, $thf(W)),bind(K, $thf(V)),bind(L, $thf(U)),bind(M, $thf(T)),bind(N, $thf(S)),bind(O, $thf(R)),bind(P, $thf(Q))]])).
% 88.18/39.56  thf(19682,plain,(! [A:mworld] : ((~ (v15 @ A)))),inference(simp,[status(thm)],[19681])).
% 88.18/39.56  thf(19684,plain,(($false)),inference(rewrite,[status(thm)],[11394,19682])).
% 88.18/39.56  thf(19685,plain,(($false)),inference(simp,[status(thm)],[19684])).
% 88.18/39.56  % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 88.18/39.56  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------