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

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

% Computer : n026.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 63.22s 25.04s
% Output   : Refutation 63.87s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SYO905^6 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20  % Computer : n026.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:29:27 UTC 2026
% 0.09/0.20  % CPUTime  : 
% 0.09/0.20  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.86/0.78  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.94/1.13  % [INFO] 	 Parsing done (351ms). 
% 1.94/1.14  % [INFO] 	 Running in sequential loop mode. 
% 2.84/1.53  % [INFO] 	 eprover registered as external prover. 
% 2.84/1.54  % [INFO] 	 Scanning for conjecture ... 
% 3.30/1.71  % [INFO] 	 Found a conjecture (or negated_conjecture) and 52 axioms. Running axiom selection ... 
% 3.55/1.82  % [INFO] 	 Axiom selection finished. Selected 52 axioms (removed 0 axioms). 
% 3.94/1.96  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 3.94/1.97  % [INFO] 	 Type checking passed. 
% 3.94/1.98  % [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 ... 
% 63.22/25.03  % [INFO] 	 Killing All external provers ... 
% 63.22/25.04  % Time passed: 24697ms (effective reasoning time: 23884ms)
% 63.22/25.04  % Axioms used in derivation (8): mod11, mod15, mod25, mod45, mod19, mrel_universal, mod49, alt1
% 63.22/25.04  % No. of inferences in proof: 140
% 63.22/25.04  % SZS status ContradictoryAxioms for /export/starexec/sandbox/benchmark/theBenchmark.p : 24697 ms resp. 23884 ms w/o parsing
% 63.87/25.27  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.87/25.27  thf(mworld_type, type, mworld: $tType).
% 63.87/25.27  thf(mrel_decl, type, mrel: (mworld > (mworld > $o))).
% 63.87/25.27  thf(mactual_decl, type, mactual: mworld).
% 63.87/25.27  thf(mlocal_decl, type, mlocal: ((mworld > $o) > $o)).
% 63.87/25.27  thf(mnot_decl, type, mnot: ((mworld > $o) > (mworld > $o))).
% 63.87/25.27  thf(mand_decl, type, mand: ((mworld > $o) > ((mworld > $o) > (mworld > $o)))).
% 63.87/25.27  thf(mor_decl, type, mor: ((mworld > $o) > ((mworld > $o) > (mworld > $o)))).
% 63.87/25.27  thf(mbox_decl, type, mbox: ((mworld > $o) > (mworld > $o))).
% 63.87/25.27  thf(mdia_decl, type, mdia: ((mworld > $o) > (mworld > $o))).
% 63.87/25.27  thf(v1_decl, type, v1: (mworld > $o)).
% 63.87/25.27  thf(v5_decl, type, v5: (mworld > $o)).
% 63.87/25.27  thf(v6_decl, type, v6: (mworld > $o)).
% 63.87/25.27  thf(v7_decl, type, v7: (mworld > $o)).
% 63.87/25.27  thf(v8_decl, type, v8: (mworld > $o)).
% 63.87/25.27  thf(v12_decl, type, v12: (mworld > $o)).
% 63.87/25.27  thf(v11_decl, type, v11: (mworld > $o)).
% 63.87/25.27  thf(v14_decl, type, v14: (mworld > $o)).
% 63.87/25.27  thf(v13_decl, type, v13: (mworld > $o)).
% 63.87/25.27  thf(v16_decl, type, v16: (mworld > $o)).
% 63.87/25.27  thf(v15_decl, type, v15: (mworld > $o)).
% 63.87/25.27  thf(v21_decl, type, v21: (mworld > $o)).
% 63.87/25.27  thf(v23_decl, type, v23: (mworld > $o)).
% 63.87/25.27  thf(v22_decl, type, v22: (mworld > $o)).
% 63.87/25.27  thf(v25_decl, type, v25: (mworld > $o)).
% 63.87/25.27  thf(v24_decl, type, v24: (mworld > $o)).
% 63.87/25.27  thf(v26_decl, type, v26: (mworld > $o)).
% 63.87/25.27  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)))))))))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))).
% 63.87/25.27  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))))))))))))))))))))).
% 63.87/25.27  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)))))))))))))))))))).
% 63.87/25.27  thf(sk14_decl, type, sk14: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))))).
% 63.87/25.27  thf(sk15_decl, type, sk15: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))))).
% 63.87/25.27  thf(sk16_decl, type, sk16: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))))).
% 63.87/25.27  thf(sk17_decl, type, sk17: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))).
% 63.87/25.27  thf(sk18_decl, type, sk18: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))))).
% 63.87/25.27  thf(sk19_decl, type, sk19: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))).
% 63.87/25.27  thf(sk20_decl, type, sk20: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))))).
% 63.87/25.27  thf(sk21_decl, type, sk21: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))).
% 63.87/25.27  thf(sk22_decl, type, sk22: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))))).
% 63.87/25.27  thf(sk23_decl, type, sk23: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))).
% 63.87/25.27  thf(sk24_decl, type, sk24: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))))).
% 63.87/25.27  thf(sk25_decl, type, sk25: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))))).
% 63.87/25.27  thf(sk26_decl, type, sk26: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))))).
% 63.87/25.27  thf(sk27_decl, type, sk27: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))))).
% 63.87/25.27  thf(sk28_decl, type, sk28: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))))).
% 63.87/25.27  thf(sk29_decl, type, sk29: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))).
% 63.87/25.27  thf(sk30_decl, type, sk30: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))))).
% 63.87/25.27  thf(sk31_decl, type, sk31: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))).
% 63.87/25.27  thf(sk32_decl, type, sk32: (mworld > (mworld > (mworld > (mworld > (mworld > (mworld > mworld))))))).
% 63.87/25.27  thf(sk33_decl, type, sk33: (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))).
% 63.87/25.27  thf(sk34_decl, type, sk34: (mworld > (mworld > (mworld > (mworld > (mworld > mworld)))))).
% 63.87/25.27  thf(sk35_decl, type, sk35: (mworld > (mworld > (mworld > (mworld > mworld))))).
% 63.87/25.27  thf(sk36_decl, type, sk36: (mworld > (mworld > (mworld > (mworld > mworld))))).
% 63.87/25.27  thf(sk37_decl, type, sk37: (mworld > (mworld > (mworld > mworld)))).
% 63.87/25.27  thf(sk38_decl, type, sk38: (mworld > (mworld > mworld))).
% 63.87/25.27  thf(sk39_decl, type, sk39: (mworld > mworld)).
% 63.87/25.27  thf(sk40_decl, type, sk40: mworld).
% 63.87/25.27  thf(mlocal_def, definition, mlocal = (^ [A:(mworld > $o)]: (A @ mactual)) ).
% 63.87/25.27  thf(mnot_def, definition, mnot = (^ [A:(mworld > $o),B:mworld]: ~ (A @ B)) ).
% 63.87/25.27  thf(mand_def, definition, mand = (^ [A:(mworld > $o),B:(mworld > $o),C:mworld]: ((A @ C) & (B @ C))) ).
% 63.87/25.27  thf(mor_def, definition, mor = (^ [A:(mworld > $o),B:(mworld > $o),C:mworld]: ((A @ C) | (B @ C))) ).
% 63.87/25.27  thf(mbox_def, definition, mbox = (^ [A:(mworld > $o),B:mworld]: ! [C:mworld]: ((mrel @ B @ C) => (A @ C))) ).
% 63.87/25.27  thf(mdia_def, definition, mdia = (^ [A:(mworld > $o),B:mworld]: ? [C:mworld]: ((mrel @ B @ C) & (A @ C))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  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)))) ).
% 63.87/25.27  thf(sk31_def, definition, sk31 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld]: (@+ [G:mworld]: ((mrel @ A @ G) & (v22 @ G)))) ).
% 63.87/25.27  thf(sk32_def, definition, sk32 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld,F:mworld]: (@+ [G:mworld]: ((mrel @ A @ G) & ~ (v22 @ G)))) ).
% 63.87/25.27  thf(sk33_def, definition, sk33 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld]: (@+ [F:mworld]: ((mrel @ A @ F) & (v23 @ F)))) ).
% 63.87/25.27  thf(sk34_def, definition, sk34 = (^ [A:mworld,B:mworld,C:mworld,D:mworld,E:mworld]: (@+ [F:mworld]: ((mrel @ A @ F) & ~ (v23 @ F)))) ).
% 63.87/25.27  thf(sk35_def, definition, sk35 = (^ [A:mworld,B:mworld,C:mworld,D:mworld]: (@+ [E:mworld]: ((mrel @ A @ E) & (v24 @ E)))) ).
% 63.87/25.27  thf(sk36_def, definition, sk36 = (^ [A:mworld,B:mworld,C:mworld,D:mworld]: (@+ [E:mworld]: ((mrel @ A @ E) & ~ (v24 @ E)))) ).
% 63.87/25.27  thf(sk37_def, definition, sk37 = (^ [A:mworld,B:mworld,C:mworld]: (@+ [D:mworld]: (mrel @ A @ D))) ).
% 63.87/25.27  thf(sk38_def, definition, sk38 = (^ [A:mworld,B:mworld]: (@+ [C:mworld]: (mrel @ A @ C))) ).
% 63.87/25.27  thf(sk39_def, definition, sk39 = (^ [A:mworld]: (@+ [B:mworld]: (mrel @ A @ B))) ).
% 63.87/25.27  thf(sk40_def, definition, sk40 = (@+ [A:mworld]: (mrel @ mactual @ A)) ).
% 63.87/25.27  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/sandbox/benchmark/theBenchmark.p',alt1)).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(3,axiom,((! [A:mworld,B:mworld]: (mrel @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_universal)).
% 63.87/25.27  thf(56,plain,((! [A:mworld,B:mworld]: (mrel @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 63.87/25.27  thf(57,plain,(! [B:mworld,A:mworld] : ((mrel @ A @ B))),inference(cnf,[status(esa)],[56])).
% 63.87/25.27  thf(5159,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])).
% 63.87/25.27  thf(5160,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)],[5159])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(3856,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])).
% 63.87/25.27  thf(3857,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)],[3856])).
% 63.87/25.27  thf(21,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v11 @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v8) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v5) @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v1)))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod49)).
% 63.87/25.27  thf(92,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) => ((v11 @ R) | ! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ 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)],[21])).
% 63.87/25.27  thf(93,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)) | (v11 @ R) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ 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)],[92])).
% 63.87/25.27  thf(1770,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)) | (v11 @ A) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v8 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v5 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v1 @ D)))),inference(rewrite,[status(thm)],[93,57])).
% 63.87/25.27  thf(1771,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v11 @ A) | (~ (v8 @ B)) | (~ (v5 @ C)) | (~ (v1 @ D)))),inference(simp,[status(thm)],[1770])).
% 63.87/25.27  thf(3858,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] : ((v11 @ U) | ~ (($true)) | (~ (v5 @ W)) | (~ (v1 @ 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)],[3857,1771])).
% 63.87/25.27  thf(3859,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] : ((v11 @ U) | (~ (v5 @ W)) | (~ (v1 @ 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)],[3858])).
% 63.87/25.27  thf(3860,plain,(! [C:mworld,B:mworld,A:mworld] : ((v11 @ A) | (~ (v5 @ B)) | (~ (v1 @ C)))),inference(pattern_uni,[status(thm)],[3859:[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(N)),bind(V, $thf(sk11 @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR))]])).
% 63.87/25.27  thf(3861,plain,(! [C:mworld,B:mworld,A:mworld] : ((v11 @ A) | (~ (v5 @ B)) | (~ (v1 @ C)))),inference(simp,[status(thm)],[3860])).
% 63.87/25.27  thf(5164,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] : ((v11 @ X) | ~ (($true)) | (~ (v1 @ 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)],[5160,3861])).
% 63.87/25.27  thf(5165,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] : ((v11 @ X) | (~ (v1 @ 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)],[5164])).
% 63.87/25.27  thf(5166,plain,(! [B:mworld,A:mworld] : ((v11 @ A) | (~ (v1 @ B)))),inference(pattern_uni,[status(thm)],[5165:[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))]])).
% 63.87/25.27  thf(5171,plain,(! [B:mworld,A:mworld] : ((v11 @ A) | (~ (v1 @ B)))),inference(simp,[status(thm)],[5166])).
% 63.87/25.27  thf(23,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v26) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v22 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v6 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v1))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod15)).
% 63.87/25.27  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) => ((v22 @ 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) => ((v6 @ 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) => (v1 @ ZB)))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 63.87/25.27  thf(97,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)) | (~ (v26 @ C)) | (~ (mrel @ C @ D)) | (~ (mrel @ D @ E)) | (~ (mrel @ E @ F)) | (~ (mrel @ F @ G)) | (v22 @ 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)) | (v6 @ W) | (~ (mrel @ W @ X)) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (~ (mrel @ Z @ ZA)) | (~ (mrel @ ZA @ ZB)) | (v1 @ ZB))),inference(cnf,[status(esa)],[96])).
% 63.87/25.27  thf(2006,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v26 @ A)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v22 @ B) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v6 @ C) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v1 @ D))),inference(rewrite,[status(thm)],[97,57])).
% 63.87/25.27  thf(2007,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (v22 @ B) | (v6 @ C) | (v1 @ D))),inference(simp,[status(thm)],[2006])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(2017,plain,(! [J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (v6 @ C) | (v1 @ D) | ~ (($true)) | ((v22 @ B) != (v22 @ (sk32 @ J @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[2007,252])).
% 63.87/25.27  thf(2018,plain,(! [J:mworld,I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (v6 @ C) | (v1 @ D) | ((v22 @ B) != (v22 @ (sk32 @ J @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[2017])).
% 63.87/25.27  thf(2019,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (v6 @ B) | (v1 @ C))),inference(pattern_uni,[status(thm)],[2018:[bind(A, $thf(+)),bind(B, $thf(sk32 @ K @ L @ M @ N @ O @ P)),bind(C, $thf(?)),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))]])).
% 63.87/25.27  thf(2037,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (v6 @ B) | (v1 @ C))),inference(simp,[status(thm)],[2019])).
% 63.87/25.27  thf(148,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 @ (sk8 @ 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])).
% 63.87/25.27  thf(4352,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 @ (sk8 @ 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)],[148,57])).
% 63.87/25.27  thf(4353,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 @ (sk8 @ 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)],[4352])).
% 63.87/25.27  thf(4387,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] : ((~ (v26 @ A)) | (v1 @ C) | ~ (($true)) | ((v6 @ B) != (v6 @ (sk8 @ 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)],[2037,4353])).
% 63.87/25.27  thf(4388,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] : ((~ (v26 @ A)) | (v1 @ C) | ((v6 @ B) != (v6 @ (sk8 @ 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)],[4387])).
% 63.87/25.27  thf(4389,plain,(! [B:mworld,A:mworld] : ((~ (v26 @ A)) | (v1 @ B))),inference(pattern_uni,[status(thm)],[4388:[bind(A, $thf(A)),bind(B, $thf(sk8 @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU)),bind(C, $thf(C)),bind(D, $thf(ZU)),bind(E, $thf(ZT)),bind(F, $thf(ZS)),bind(G, $thf(ZR)),bind(H, $thf(ZQ)),bind(I, $thf(ZP)),bind(J, $thf(ZO)),bind(K, $thf(ZN)),bind(L, $thf(ZM)),bind(M, $thf(ZL)),bind(N, $thf(ZK)),bind(O, $thf(ZJ)),bind(P, $thf(ZI)),bind(Q, $thf(ZH)),bind(R, $thf(ZG)),bind(S, $thf(ZF)),bind(T, $thf(ZE)),bind(U, $thf(ZD)),bind(V, $thf(ZC)),bind(W, $thf(ZB)),bind(X, $thf(ZA)),bind(Y, $thf(Z))]])).
% 63.87/25.27  thf(4398,plain,(! [B:mworld,A:mworld] : ((~ (v26 @ A)) | (v1 @ B))),inference(simp,[status(thm)],[4389])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(5092,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])).
% 63.87/25.27  thf(5093,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)],[5092])).
% 63.87/25.27  thf(145,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 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[105])).
% 63.87/25.27  thf(4143,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 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(rewrite,[status(thm)],[145,57])).
% 63.87/25.27  thf(4144,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 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)))),inference(simp,[status(thm)],[4143])).
% 63.87/25.27  thf(25,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mor @ v26 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v14) @ (mbox @ (mbox @ (mor @ v12 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v5)))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod11)).
% 63.87/25.27  thf(100,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) => (! [L:mworld]: ((mrel @ K @ L) => (! [M:mworld]: ((mrel @ L @ M) => (! [N:mworld]: ((mrel @ M @ N) => (! [O:mworld]: ((mrel @ N @ O) => (~ (v14 @ O) | ! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => ((v12 @ 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))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 63.87/25.27  thf(101,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] : ((~ (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)) | (~ (mrel @ K @ L)) | (~ (mrel @ L @ M)) | (~ (mrel @ M @ N)) | (~ (mrel @ N @ O)) | (~ (v14 @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (v12 @ Q) | (~ (mrel @ Q @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (mrel @ V @ W)) | (~ (mrel @ W @ X)) | (~ (v5 @ X)))),inference(cnf,[status(esa)],[100])).
% 63.87/25.27  thf(2310,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | (v26 @ A) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v14 @ B)) | ~ (($true)) | ~ (($true)) | (v12 @ C) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v5 @ D)))),inference(rewrite,[status(thm)],[101,57])).
% 63.87/25.27  thf(2311,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (~ (v14 @ B)) | (v12 @ C) | (~ (v5 @ D)))),inference(simp,[status(thm)],[2310])).
% 63.87/25.27  thf(4147,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] : ((v26 @ O) | ~ (($true)) | (v12 @ Q) | (~ (v5 @ R)) | ((v14 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v14 @ P)))),inference(paramod_ordered,[status(thm)],[4144,2311])).
% 63.87/25.27  thf(4148,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] : ((v26 @ O) | (v12 @ Q) | (~ (v5 @ R)) | ((v14 @ (sk19 @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v14 @ P)))),inference(simp,[status(thm)],[4147])).
% 63.87/25.27  thf(4149,plain,(! [C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (v12 @ B) | (~ (v5 @ C)))),inference(pattern_uni,[status(thm)],[4148:[bind(A, $thf(ZF)),bind(B, $thf(ZE)),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(=)),bind(P, $thf(sk19 @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF))]])).
% 63.87/25.27  thf(4151,plain,(! [C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (v12 @ B) | (~ (v5 @ C)))),inference(simp,[status(thm)],[4149])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(236,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v24 @ (sk35 @ D @ C @ B @ A)))),inference(simp,[status(thm)],[235])).
% 63.87/25.27  thf(12,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v13 @ (mbox @ (mnot @ v12))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod19)).
% 63.87/25.27  thf(74,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => ((v25 @ D) | ! [E:mworld]: ((mrel @ D @ E) => (~ (v24 @ 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) => (~ (v12 @ Q))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 63.87/25.27  thf(75,plain,(! [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)) | (v25 @ D) | (~ (mrel @ D @ E)) | (~ (v24 @ 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)) | (~ (v12 @ Q)))),inference(cnf,[status(esa)],[74])).
% 63.87/25.27  thf(933,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v25 @ A) | ~ (($true)) | (~ (v24 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (v13 @ C) | ~ (($true)) | (~ (v12 @ D)))),inference(rewrite,[status(thm)],[75,57])).
% 63.87/25.27  thf(934,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((v25 @ A) | (~ (v24 @ B)) | (v13 @ C) | (~ (v12 @ D)))),inference(simp,[status(thm)],[933])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(328,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])).
% 63.87/25.27  thf(329,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)],[328])).
% 63.87/25.27  thf(938,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] : ((v25 @ A) | (~ (v24 @ B)) | (~ (v12 @ D)) | ~ (($true)) | ((v13 @ C) != (v13 @ (sk18 @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[934,329])).
% 63.87/25.27  thf(939,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] : ((v25 @ A) | (~ (v24 @ B)) | (~ (v12 @ D)) | ((v13 @ C) != (v13 @ (sk18 @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[938])).
% 63.87/25.27  thf(940,plain,(! [C:mworld,B:mworld,A:mworld] : ((v25 @ A) | (~ (v24 @ B)) | (~ (v12 @ C)))),inference(pattern_uni,[status(thm)],[939:[bind(A, $thf(7)),bind(B, $thf(8)),bind(C, $thf(sk18 @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH)),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))]])).
% 63.87/25.27  thf(949,plain,(! [C:mworld,B:mworld,A:mworld] : ((v25 @ A) | (~ (v24 @ B)) | (~ (v12 @ C)))),inference(simp,[status(thm)],[940])).
% 63.87/25.27  thf(982,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v25 @ E) | ~ (($true)) | (~ (v12 @ G)) | ((v24 @ (sk35 @ D @ C @ B @ A)) != (v24 @ F)))),inference(paramod_ordered,[status(thm)],[236,949])).
% 63.87/25.27  thf(983,plain,(! [G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v25 @ E) | (~ (v12 @ G)) | ((v24 @ (sk35 @ D @ C @ B @ A)) != (v24 @ F)))),inference(simp,[status(thm)],[982])).
% 63.87/25.27  thf(984,plain,(! [B:mworld,A:mworld] : ((v25 @ A) | (~ (v12 @ B)))),inference(pattern_uni,[status(thm)],[983:[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))]])).
% 63.87/25.27  thf(990,plain,(! [B:mworld,A:mworld] : ((v25 @ A) | (~ (v12 @ B)))),inference(simp,[status(thm)],[984])).
% 63.87/25.27  thf(15,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v25) @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v12) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v6))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod25)).
% 63.87/25.27  thf(80,plain,((! [A:mworld]: ((mrel @ mactual @ A) => (! [B:mworld]: ((mrel @ A @ B) => (! [C:mworld]: ((mrel @ B @ C) => (! [D:mworld]: ((mrel @ C @ D) => (~ (v25 @ 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) => (! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (~ (v12 @ 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)],[15])).
% 63.87/25.27  thf(81,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)) | (~ (v25 @ 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)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (v12 @ 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)],[80])).
% 63.87/25.27  thf(1106,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v25 @ A)) | ~ (($true)) | ~ (($true)) | (v23 @ B) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v12 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v6 @ D)))),inference(rewrite,[status(thm)],[81,57])).
% 63.87/25.27  thf(1107,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v25 @ A)) | (v23 @ B) | (~ (v12 @ C)) | (~ (v6 @ D)))),inference(simp,[status(thm)],[1106])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(1162,plain,(! [I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v25 @ A)) | (~ (v12 @ C)) | (~ (v6 @ D)) | ~ (($true)) | ((v23 @ B) != (v23 @ (sk34 @ I @ H @ G @ F @ E))))),inference(paramod_ordered,[status(thm)],[1107,232])).
% 63.87/25.27  thf(1163,plain,(! [I:mworld,H:mworld,G:mworld,F:mworld,E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v25 @ A)) | (~ (v12 @ C)) | (~ (v6 @ D)) | ((v23 @ B) != (v23 @ (sk34 @ I @ H @ G @ F @ E))))),inference(simp,[status(thm)],[1162])).
% 63.87/25.27  thf(1164,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v25 @ A)) | (~ (v12 @ B)) | (~ (v6 @ C)))),inference(pattern_uni,[status(thm)],[1163:[bind(A, $thf(1)),bind(B, $thf(sk34 @ J @ K @ L @ M @ N)),bind(C, $thf(>)),bind(D, $thf(D)),bind(E, $thf(N)),bind(F, $thf(M)),bind(G, $thf(L)),bind(H, $thf(K)),bind(I, $thf(J))]])).
% 63.87/25.27  thf(1173,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v25 @ A)) | (~ (v12 @ B)) | (~ (v6 @ C)))),inference(simp,[status(thm)],[1164])).
% 63.87/25.27  thf(1252,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v12 @ B)) | ~ (($true)) | (~ (v12 @ D)) | (~ (v6 @ E)) | ((v25 @ A) != (v25 @ C)))),inference(paramod_ordered,[status(thm)],[990,1173])).
% 63.87/25.27  thf(1253,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v12 @ B)) | (~ (v12 @ D)) | (~ (v6 @ E)) | ((v25 @ A) != (v25 @ C)))),inference(simp,[status(thm)],[1252])).
% 63.87/25.27  thf(1254,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v12 @ A)) | (~ (v12 @ B)) | (~ (v6 @ C)))),inference(pattern_uni,[status(thm)],[1253:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(A))]])).
% 63.87/25.27  thf(1283,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v12 @ A)) | (~ (v12 @ B)) | (~ (v6 @ C)))),inference(simp,[status(thm)],[1254])).
% 63.87/25.27  thf(1393,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v12 @ A)) | (~ (v6 @ C)) | ((v12 @ B) != (v12 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[1283])).
% 63.87/25.27  thf(1394,plain,(! [B:mworld,A:mworld] : ((~ (v12 @ A)) | (~ (v6 @ B)))),inference(pattern_uni,[status(thm)],[1393:[bind(A, $thf(B))]])).
% 63.87/25.27  thf(1406,plain,(! [B:mworld,A:mworld] : ((~ (v12 @ A)) | (~ (v6 @ B)))),inference(simp,[status(thm)],[1394])).
% 63.87/25.27  thf(4158,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ C)) | ~ (($true)) | (~ (v6 @ E)) | ((v12 @ B) != (v12 @ D)))),inference(paramod_ordered,[status(thm)],[4151,1406])).
% 63.87/25.27  thf(4159,plain,(! [E:mworld,D:mworld,C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ C)) | (~ (v6 @ E)) | ((v12 @ B) != (v12 @ D)))),inference(simp,[status(thm)],[4158])).
% 63.87/25.27  thf(4160,plain,(! [C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ B)) | (~ (v6 @ C)))),inference(pattern_uni,[status(thm)],[4159:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(B))]])).
% 63.87/25.27  thf(4194,plain,(! [C:mworld,B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ B)) | (~ (v6 @ C)))),inference(simp,[status(thm)],[4160])).
% 63.87/25.27  thf(5105,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] : ((v26 @ W) | (~ (v5 @ X)) | ~ (($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 @ Y)))),inference(paramod_ordered,[status(thm)],[5093,4194])).
% 63.87/25.27  thf(5106,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] : ((v26 @ W) | (~ (v5 @ X)) | ((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 @ Y)))),inference(simp,[status(thm)],[5105])).
% 63.87/25.27  thf(5107,plain,(! [B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ B)))),inference(pattern_uni,[status(thm)],[5106:[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(X)),bind(Y, $thf(sk7 @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU))]])).
% 63.87/25.27  thf(5121,plain,(! [B:mworld,A:mworld] : ((v26 @ A) | (~ (v5 @ B)))),inference(simp,[status(thm)],[5107])).
% 63.87/25.27  thf(5200,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] : ((v26 @ X) | ~ (($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)) != (v5 @ Y)))),inference(paramod_ordered,[status(thm)],[5160,5121])).
% 63.87/25.27  thf(5201,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] : ((v26 @ X) | ((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)],[5200])).
% 63.87/25.27  thf(5202,plain,(! [A:mworld] : ((v26 @ A))),inference(pattern_uni,[status(thm)],[5201:[bind(A, $thf(ZV)),bind(B, $thf(ZU)),bind(C, $thf(ZT)),bind(D, $thf(ZS)),bind(E, $thf(ZR)),bind(F, $thf(ZQ)),bind(G, $thf(ZP)),bind(H, $thf(ZO)),bind(I, $thf(ZN)),bind(J, $thf(ZM)),bind(K, $thf(ZL)),bind(L, $thf(ZK)),bind(M, $thf(ZJ)),bind(N, $thf(ZI)),bind(O, $thf(ZH)),bind(P, $thf(ZG)),bind(Q, $thf(ZF)),bind(R, $thf(ZE)),bind(S, $thf(ZD)),bind(T, $thf(ZC)),bind(U, $thf(ZB)),bind(V, $thf(ZA)),bind(W, $thf(Z)),bind(X, $thf(X)),bind(Y, $thf(sk5 @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS @ ZT @ ZU @ ZV))]])).
% 63.87/25.27  thf(5212,plain,(! [A:mworld] : ((v26 @ A))),inference(simp,[status(thm)],[5202])).
% 63.87/25.27  thf(5218,plain,(! [A:mworld] : (~ (($true)) | (v1 @ A))),inference(rewrite,[status(thm)],[4398,5212])).
% 63.87/25.27  thf(5219,plain,(! [A:mworld] : ((v1 @ A))),inference(simp,[status(thm)],[5218])).
% 63.87/25.27  thf(5223,plain,(! [A:mworld] : ((v1 @ A))),inference(simp,[status(thm)],[5219])).
% 63.87/25.27  thf(152,plain,(! [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)) | (v7 @ (sk9 @ 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])).
% 63.87/25.27  thf(4720,plain,(! [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)) | (v7 @ (sk9 @ 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)],[152,57])).
% 63.87/25.27  thf(4721,plain,(! [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] : ((v7 @ (sk9 @ 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)],[4720])).
% 63.87/25.27  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])).
% 63.87/25.27  thf(3674,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])).
% 63.87/25.27  thf(3675,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)],[3674])).
% 63.87/25.27  thf(26,axiom,((mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v11) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v7) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v1)))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod45)).
% 63.87/25.27  thf(102,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) => (~ (v15 @ N) | ! [O:mworld]: ((mrel @ N @ O) => (! [P:mworld]: ((mrel @ O @ P) => (! [Q:mworld]: ((mrel @ P @ Q) => (! [R:mworld]: ((mrel @ Q @ R) => (~ (v11 @ R) | ! [S:mworld]: ((mrel @ R @ S) => (! [T:mworld]: ((mrel @ S @ T) => (! [U:mworld]: ((mrel @ T @ U) => (! [V:mworld]: ((mrel @ U @ V) => (~ (v7 @ 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) => (~ (v1 @ ZB))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 63.87/25.27  thf(103,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)) | (~ (v15 @ N)) | (~ (mrel @ N @ O)) | (~ (mrel @ O @ P)) | (~ (mrel @ P @ Q)) | (~ (mrel @ Q @ R)) | (~ (v11 @ R)) | (~ (mrel @ R @ S)) | (~ (mrel @ S @ T)) | (~ (mrel @ T @ U)) | (~ (mrel @ U @ V)) | (~ (v7 @ V)) | (~ (mrel @ V @ W)) | (~ (mrel @ W @ X)) | (~ (mrel @ X @ Y)) | (~ (mrel @ Y @ Z)) | (~ (mrel @ Z @ ZA)) | (~ (mrel @ ZA @ ZB)) | (~ (v1 @ ZB)))),inference(cnf,[status(esa)],[102])).
% 63.87/25.27  thf(2468,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : (~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v15 @ A)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v11 @ B)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v7 @ C)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (v1 @ D)))),inference(rewrite,[status(thm)],[103,57])).
% 63.87/25.27  thf(2469,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v15 @ A)) | (~ (v11 @ B)) | (~ (v7 @ C)) | (~ (v1 @ D)))),inference(simp,[status(thm)],[2468])).
% 63.87/25.27  thf(3676,plain,(! [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)) | (~ (v11 @ O)) | (~ (v7 @ P)) | (~ (v1 @ Q)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ N)))),inference(paramod_ordered,[status(thm)],[3675,2469])).
% 63.87/25.27  thf(3677,plain,(! [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] : ((~ (v11 @ O)) | (~ (v7 @ P)) | (~ (v1 @ Q)) | ((v15 @ (sk21 @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v15 @ N)))),inference(simp,[status(thm)],[3676])).
% 63.87/25.27  thf(3678,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v11 @ A)) | (~ (v7 @ B)) | (~ (v1 @ C)))),inference(pattern_uni,[status(thm)],[3677:[bind(A, $thf(ZD)),bind(B, $thf(ZC)),bind(C, $thf(ZB)),bind(D, $thf(ZA)),bind(E, $thf(Z)),bind(F, $thf(Y)),bind(G, $thf(X)),bind(H, $thf(W)),bind(I, $thf(V)),bind(J, $thf(U)),bind(K, $thf(T)),bind(L, $thf(S)),bind(M, $thf(R)),bind(N, $thf(sk21 @ R @ S @ T @ U @ V @ W @ X @ Y @ Z @ ZA @ ZB @ ZC @ ZD))]])).
% 63.87/25.27  thf(3682,plain,(! [C:mworld,B:mworld,A:mworld] : ((~ (v11 @ A)) | (~ (v7 @ B)) | (~ (v1 @ C)))),inference(simp,[status(thm)],[3678])).
% 63.87/25.27  thf(4728,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] : ((~ (v11 @ V)) | ~ (($true)) | (~ (v1 @ X)) | ((v7 @ (sk9 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v7 @ W)))),inference(paramod_ordered,[status(thm)],[4721,3682])).
% 63.87/25.27  thf(4729,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] : ((~ (v11 @ V)) | (~ (v1 @ X)) | ((v7 @ (sk9 @ U @ T @ S @ R @ Q @ P @ O @ N @ M @ L @ K @ J @ I @ H @ G @ F @ E @ D @ C @ B @ A)) != (v7 @ W)))),inference(simp,[status(thm)],[4728])).
% 63.87/25.27  thf(4730,plain,(! [B:mworld,A:mworld] : ((~ (v11 @ A)) | (~ (v1 @ B)))),inference(pattern_uni,[status(thm)],[4729:[bind(A, $thf(ZS)),bind(B, $thf(ZR)),bind(C, $thf(ZQ)),bind(D, $thf(ZP)),bind(E, $thf(ZO)),bind(F, $thf(ZN)),bind(G, $thf(ZM)),bind(H, $thf(ZL)),bind(I, $thf(ZK)),bind(J, $thf(ZJ)),bind(K, $thf(ZI)),bind(L, $thf(ZH)),bind(M, $thf(ZG)),bind(N, $thf(ZF)),bind(O, $thf(ZE)),bind(P, $thf(ZD)),bind(Q, $thf(ZC)),bind(R, $thf(ZB)),bind(S, $thf(ZA)),bind(T, $thf(Z)),bind(U, $thf(Y)),bind(V, $thf(V)),bind(W, $thf(sk9 @ Y @ Z @ ZA @ ZB @ ZC @ ZD @ ZE @ ZF @ ZG @ ZH @ ZI @ ZJ @ ZK @ ZL @ ZM @ ZN @ ZO @ ZP @ ZQ @ ZR @ ZS))]])).
% 63.87/25.27  thf(4751,plain,(! [B:mworld,A:mworld] : ((~ (v11 @ A)) | (~ (v1 @ B)))),inference(simp,[status(thm)],[4730])).
% 63.87/25.27  thf(4953,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (~ (v11 @ C)) | ~ (($true)) | ((v1 @ B) != (v1 @ D)))),inference(paramod_ordered,[status(thm)],[4398,4751])).
% 63.87/25.27  thf(4954,plain,(! [D:mworld,C:mworld,B:mworld,A:mworld] : ((~ (v26 @ A)) | (~ (v11 @ C)) | ((v1 @ B) != (v1 @ D)))),inference(simp,[status(thm)],[4953])).
% 63.87/25.27  thf(4955,plain,(! [B:mworld,A:mworld] : ((~ (v26 @ A)) | (~ (v11 @ B)))),inference(pattern_uni,[status(thm)],[4954:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(B))]])).
% 63.87/25.27  thf(4982,plain,(! [B:mworld,A:mworld] : ((~ (v26 @ A)) | (~ (v11 @ B)))),inference(simp,[status(thm)],[4955])).
% 63.87/25.27  thf(5220,plain,(! [A:mworld] : (~ (($true)) | (~ (v11 @ A)))),inference(rewrite,[status(thm)],[4982,5212])).
% 63.87/25.27  thf(5221,plain,(! [A:mworld] : ((~ (v11 @ A)))),inference(simp,[status(thm)],[5220])).
% 63.87/25.27  thf(5224,plain,(! [A:mworld] : ((~ (v11 @ A)))),inference(simp,[status(thm)],[5221])).
% 63.87/25.27  thf(5239,plain,(($false) | ~ (($true))),inference(rewrite,[status(thm)],[5171,5223,5224])).
% 63.87/25.27  thf(5240,plain,(($false)),inference(simp,[status(thm)],[5239])).
% 63.87/25.27  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.87/25.27  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------