%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NLP251+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:01:57 EDT 2024 % Result : Theorem 116.67s 116.73s % Output : CNFRefutation 116.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP251+1 : TPTP v8.2.0. Released v2.4.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 01:34:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.44/0.57 start to proof:theBenchmark % 116.67/116.70 %------------------------------------------- % 116.67/116.70 % File :CSE---1.7 % 116.67/116.70 % Problem :theBenchmark % 116.67/116.70 % Transform :cnf % 116.67/116.70 % Format :tptp:raw % 116.67/116.70 % Command :java -jar mcs_scs.jar %d %s % 116.67/116.70 % 116.67/116.70 % Result :Theorem 116.070000s % 116.67/116.70 % Output :CNFRefutation 116.070000s % 116.67/116.70 %------------------------------------------- % 116.67/116.71 %-------------------------------------------------------------------------- % 116.67/116.71 % File : NLP251+1 : TPTP v8.2.0. Released v2.4.0. % 116.67/116.71 % Domain : Natural Language Processing % 116.67/116.71 % Problem : Vincent believes that every man smokes, problem 32 % 116.67/116.71 % Version : [Bos00b] axioms. % 116.67/116.71 % English : Eliminating non-informative interpretations in the statement % 116.67/116.71 % "Vincent believes that every man smokes. Jules is a man. % 116.67/116.71 % Vincent believes that jules smokes." % 116.67/116.71 % 116.67/116.71 % Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a % 116.67/116.71 % [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language % 116.67/116.71 % Source : [Bos00b] % 116.67/116.71 % Names : doris228 [Bos00b] % 116.67/116.71 % 116.67/116.71 % Status : Theorem % 116.67/116.71 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.13 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.33 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.48 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.11 v3.2.0, 0.33 v2.7.0, 0.00 v2.4.0 % 116.67/116.71 % Syntax : Number of formulae : 72 ( 0 unt; 0 def) % 116.67/116.71 % Number of atoms : 254 ( 3 equ) % 116.67/116.71 % Maximal formula atoms : 67 ( 3 avg) % 116.67/116.71 % Number of connectives : 190 ( 8 ~; 0 |; 109 &) % 116.67/116.71 % ( 0 <=>; 73 =>; 0 <=; 0 <~>) % 116.67/116.71 % Maximal formula depth : 57 ( 6 avg) % 116.67/116.71 % Maximal term depth : 1 ( 1 avg) % 116.67/116.71 % Number of predicates : 37 ( 36 usr; 0 prp; 1-4 aty) % 116.67/116.71 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 116.67/116.71 % Number of variables : 216 ( 190 !; 26 ?) % 116.67/116.71 % SPC : FOF_THM_RFO_SEQ % 116.67/116.71 % 116.67/116.71 % Comments : % 116.67/116.71 %-------------------------------------------------------------------------- % 116.67/116.71 fof(ax1,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( jules_forename(U,V) % 116.67/116.71 => forename(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax2,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( vincent_forename(U,V) % 116.67/116.71 => forename(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax3,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( relname(U,V) % 116.67/116.71 => relation(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax4,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( forename(U,V) % 116.67/116.71 => relname(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax5,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( man(U,V) % 116.67/116.71 => male(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax6,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.71 ( human_person(U,V) % 116.67/116.71 => animate(U,V) ) ). % 116.67/116.71 % 116.67/116.71 fof(ax7,axiom, % 116.67/116.71 ! [U,V] : % 116.67/116.72 ( human_person(U,V) % 116.67/116.72 => human(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax8,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( organism(U,V) % 116.67/116.72 => living(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax9,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( organism(U,V) % 116.67/116.72 => impartial(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax10,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( entity(U,V) % 116.67/116.72 => existent(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax11,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( entity(U,V) % 116.67/116.72 => specific(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax12,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( entity(U,V) % 116.67/116.72 => thing(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax13,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( organism(U,V) % 116.67/116.72 => entity(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax14,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( human_person(U,V) % 116.67/116.72 => organism(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax15,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( man(U,V) % 116.67/116.72 => human_person(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax16,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( state(U,V) % 116.67/116.72 => event(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax17,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( state(U,V) % 116.67/116.72 => eventuality(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax18,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( abstraction(U,V) % 116.67/116.72 => unisex(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax19,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( abstraction(U,V) % 116.67/116.72 => general(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax20,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( abstraction(U,V) % 116.67/116.72 => nonhuman(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax21,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( abstraction(U,V) % 116.67/116.72 => thing(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax22,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( relation(U,V) % 116.67/116.72 => abstraction(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax23,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( proposition(U,V) % 116.67/116.72 => relation(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax24,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( eventuality(U,V) % 116.67/116.72 => unisex(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax25,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( eventuality(U,V) % 116.67/116.72 => nonexistent(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax26,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( eventuality(U,V) % 116.67/116.72 => specific(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax27,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( thing(U,V) % 116.67/116.72 => singleton(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax28,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( eventuality(U,V) % 116.67/116.72 => thing(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax29,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( event(U,V) % 116.67/116.72 => eventuality(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax30,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( smoke(U,V) % 116.67/116.72 => event(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax31,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( existent(U,V) % 116.67/116.72 => ~ nonexistent(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax32,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( nonhuman(U,V) % 116.67/116.72 => ~ human(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax33,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( specific(U,V) % 116.67/116.72 => ~ general(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax34,axiom, % 116.67/116.72 ! [U,V] : % 116.67/116.72 ( unisex(U,V) % 116.67/116.72 => ~ male(U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax35,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & jules_forename(V,U) ) % 116.67/116.72 => jules_forename(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax36,axiom, % 116.67/116.72 ! [U,V,W,X] : % 116.67/116.72 ( ( accessible_world(W,X) % 116.67/116.72 & of(W,U,V) ) % 116.67/116.72 => of(X,U,V) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax37,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & vincent_forename(V,U) ) % 116.67/116.72 => vincent_forename(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax38,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & relname(V,U) ) % 116.67/116.72 => relname(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax39,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & forename(V,U) ) % 116.67/116.72 => forename(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax40,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & male(V,U) ) % 116.67/116.72 => male(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax41,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & animate(V,U) ) % 116.67/116.72 => animate(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax42,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & human(V,U) ) % 116.67/116.72 => human(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax43,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & living(V,U) ) % 116.67/116.72 => living(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax44,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & impartial(V,U) ) % 116.67/116.72 => impartial(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax45,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & existent(V,U) ) % 116.67/116.72 => existent(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax46,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & entity(V,U) ) % 116.67/116.72 => entity(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax47,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & organism(V,U) ) % 116.67/116.72 => organism(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax48,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & human_person(V,U) ) % 116.67/116.72 => human_person(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax49,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & man(V,U) ) % 116.67/116.72 => man(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax50,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & state(V,U) ) % 116.67/116.72 => state(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax51,axiom, % 116.67/116.72 ! [U,V,W,X,Y] : % 116.67/116.72 ( ( accessible_world(X,Y) % 116.67/116.72 & be(X,U,V,W) ) % 116.67/116.72 => be(Y,U,V,W) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax52,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & general(V,U) ) % 116.67/116.72 => general(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax53,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & nonhuman(V,U) ) % 116.67/116.72 => nonhuman(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax54,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & abstraction(V,U) ) % 116.67/116.72 => abstraction(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax55,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & relation(V,U) ) % 116.67/116.72 => relation(W,U) ) ). % 116.67/116.72 % 116.67/116.72 fof(ax56,axiom, % 116.67/116.72 ! [U,V,W] : % 116.67/116.72 ( ( accessible_world(V,W) % 116.67/116.72 & proposition(V,U) ) % 116.67/116.72 => proposition(W,U) ) ). % 116.67/116.72 % 116.67/116.73 fof(ax57,axiom, % 116.67/116.73 ! [U,V,W,X] : % 116.67/116.73 ( ( accessible_world(W,X) % 116.67/116.73 & theme(W,U,V) ) % 116.67/116.73 => theme(X,U,V) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax58,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & think_believe_consider(V,U) ) % 116.67/116.73 => think_believe_consider(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax59,axiom, % 116.67/116.73 ! [U,V,W,X] : % 116.67/116.73 ( ( accessible_world(W,X) % 116.67/116.73 & agent(W,U,V) ) % 116.67/116.73 => agent(X,U,V) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax60,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & present(V,U) ) % 116.67/116.73 => present(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax61,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & unisex(V,U) ) % 116.67/116.73 => unisex(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax62,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & nonexistent(V,U) ) % 116.67/116.73 => nonexistent(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax63,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & specific(V,U) ) % 116.67/116.73 => specific(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax64,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & singleton(V,U) ) % 116.67/116.73 => singleton(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax65,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & thing(V,U) ) % 116.67/116.73 => thing(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax66,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & eventuality(V,U) ) % 116.67/116.73 => eventuality(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax67,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & event(V,U) ) % 116.67/116.73 => event(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax68,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( accessible_world(V,W) % 116.67/116.73 & smoke(V,U) ) % 116.67/116.73 => smoke(W,U) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax69,axiom, % 116.67/116.73 ! [U,V,W] : % 116.67/116.73 ( ( entity(U,V) % 116.67/116.73 & forename(U,W) % 116.67/116.73 & of(U,W,V) ) % 116.67/116.73 => ~ ? [X] : % 116.67/116.73 ( forename(U,X) % 116.67/116.73 & X != W % 116.67/116.73 & of(U,X,V) ) ) ). % 116.67/116.73 % 116.67/116.73 fof(ax70,axiom, % 116.67/116.73 ! [U,V,W,X] : % 116.67/116.73 ( be(U,V,W,X) % 116.67/116.73 => W = X ) ). % 116.67/116.73 % 116.67/116.73 fof(ax71,axiom, % 116.67/116.73 ! [U,V,W,X,Y,Z] : % 116.67/116.73 ( ( think_believe_consider(U,V) % 116.67/116.73 & proposition(U,Y) % 116.67/116.73 & theme(U,V,Y) % 116.67/116.73 & agent(U,V,X) % 116.67/116.73 & think_believe_consider(U,W) % 116.67/116.73 & proposition(U,Z) % 116.67/116.73 & theme(U,W,Z) % 116.67/116.73 & agent(U,W,X) ) % 116.67/116.73 => Y = Z ) ). % 116.67/116.73 % 116.67/116.73 fof(co1,conjecture, % 116.67/116.73 ~ ( ? [U] : % 116.67/116.73 ( actual_world(U) % 116.67/116.73 & ? [V,W,X,Y,Z,X1,X2] : % 116.67/116.73 ( of(U,W,V) % 116.67/116.73 & man(U,V) % 116.67/116.73 & vincent_forename(U,W) % 116.67/116.73 & forename(U,W) % 116.67/116.73 & proposition(U,Y) % 116.67/116.73 & agent(U,X,V) % 116.67/116.73 & theme(U,X,Y) % 116.67/116.73 & event(U,X) % 116.67/116.73 & present(U,X) % 116.67/116.73 & think_believe_consider(U,X) % 116.67/116.73 & accessible_world(U,Y) % 116.67/116.73 & ! [X3] : % 116.67/116.73 ( man(Y,X3) % 116.67/116.73 => ? [X4] : % 116.67/116.73 ( event(Y,X4) % 116.67/116.73 & agent(Y,X4,X3) % 116.67/116.73 & present(Y,X4) % 116.67/116.73 & smoke(Y,X4) ) ) % 116.67/116.73 & of(U,Z,X1) % 116.67/116.73 & man(U,X1) % 116.67/116.73 & jules_forename(U,Z) % 116.67/116.73 & forename(U,Z) % 116.67/116.73 & man(U,X1) % 116.67/116.73 & state(U,X2) % 116.67/116.73 & be(U,X2,X1,X1) ) ) % 116.67/116.73 & ~ ? [X5] : % 116.67/116.73 ( actual_world(X5) % 116.67/116.73 & ? [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] : % 116.67/116.73 ( of(X5,X7,X6) % 116.67/116.73 & man(X5,X6) % 116.67/116.73 & vincent_forename(X5,X7) % 116.67/116.73 & forename(X5,X7) % 116.67/116.73 & of(X5,X9,X8) % 116.67/116.73 & man(X5,X8) % 116.67/116.73 & jules_forename(X5,X9) % 116.67/116.73 & forename(X5,X9) % 116.67/116.73 & of(X5,W,V) % 116.67/116.73 & man(X5,V) % 116.67/116.73 & vincent_forename(X5,W) % 116.67/116.73 & forename(X5,W) % 116.67/116.73 & proposition(X5,Y) % 116.67/116.73 & agent(X5,X,V) % 116.67/116.73 & theme(X5,X,Y) % 116.67/116.73 & event(X5,X) % 116.67/116.73 & present(X5,X) % 116.67/116.73 & think_believe_consider(X5,X) % 116.67/116.73 & accessible_world(X5,Y) % 116.67/116.73 & ! [X3] : % 116.67/116.73 ( man(Y,X3) % 116.67/116.73 => ? [X4] : % 116.67/116.73 ( event(Y,X4) % 116.67/116.73 & agent(Y,X4,X3) % 116.67/116.73 & present(Y,X4) % 116.67/116.73 & smoke(Y,X4) ) ) % 116.67/116.73 & of(X5,Z,X1) % 116.67/116.73 & man(X5,X1) % 116.67/116.73 & jules_forename(X5,Z) % 116.67/116.73 & forename(X5,Z) % 116.67/116.73 & man(X5,X1) % 116.67/116.73 & state(X5,X2) % 116.67/116.73 & be(X5,X2,X1,X1) % 116.67/116.73 & proposition(X5,X11) % 116.67/116.73 & agent(X5,X10,X6) % 116.67/116.73 & theme(X5,X10,X11) % 116.67/116.73 & event(X5,X10) % 116.67/116.73 & present(X5,X10) % 116.67/116.73 & think_believe_consider(X5,X10) % 116.67/116.73 & accessible_world(X5,X11) % 116.67/116.73 & ? [X12] : % 116.67/116.73 ( event(X11,X12) % 116.67/116.73 & agent(X11,X12,X8) % 116.67/116.73 & present(X11,X12) % 116.67/116.73 & smoke(X11,X12) ) ) ) ) ). % 116.67/116.73 % 116.67/116.73 %-------------------------------------------------------------------------- % 116.67/116.73 %------------------------------------------- % 116.67/116.73 % Proof found % 116.67/116.73 % SZS status Theorem for theBenchmark % 116.67/116.73 % SZS output start Proof % 116.67/116.73 %ClaNum:190(EqnAxiom:94) % 116.67/116.73 %VarNum:606(SingletonVarNum:224) % 116.67/116.73 %MaxLitNum:41 % 116.67/116.73 %MaxfuncDepth:1 % 116.67/116.73 %SharedTerms:26 % 116.67/116.73 %goalClause: 95 96 97 98 99 100 102 103 104 105 106 107 108 109 110 111 112 113 144 145 146 181 189 190 % 116.67/116.73 %singleGoalClaCount:18 % 116.67/116.73 [95]P1(a1) % 116.67/116.73 [96]P4(a1,a3) % 116.67/116.73 [97]P5(a1,a4) % 116.67/116.73 [98]P5(a1,a3) % 116.67/116.73 [99]P17(a1,a4) % 116.67/116.73 [100]P18(a1,a5) % 116.67/116.73 [102]P18(a1,a8) % 116.67/116.73 [103]P21(a1,a9) % 116.67/116.73 [104]P6(a1,a6) % 116.67/116.73 [105]P22(a1,a7) % 116.67/116.73 [106]P2(a1,a7) % 116.67/116.73 [107]P33(a1,a6) % 116.67/116.73 [108]P23(a1,a6) % 116.67/116.73 [109]P24(a1,a4,a5) % 116.67/116.73 [110]P24(a1,a3,a8) % 116.67/116.73 [111]P34(a1,a6,a7) % 116.67/116.73 [112]P7(a1,a6,a5) % 116.67/116.73 [113]P8(a1,a9,a8,a8) % 116.67/116.73 [144]~P18(a7,x1441)+P6(a7,f10(x1441)) % 116.67/116.73 [145]~P18(a7,x1451)+P31(a7,f10(x1451)) % 116.67/116.73 [146]~P18(a7,x1461)+P23(a7,f10(x1461)) % 116.67/116.73 [181]~P18(a7,x1811)+P7(a7,f10(x1811),x1811) % 116.67/116.73 [114]~P4(x1141,x1142)+P5(x1141,x1142) % 116.67/116.73 [115]~P17(x1151,x1152)+P5(x1151,x1152) % 116.67/116.73 [116]~P5(x1161,x1162)+P28(x1161,x1162) % 116.67/116.73 [117]~P28(x1171,x1172)+P29(x1171,x1172) % 116.67/116.73 [118]~P22(x1181,x1182)+P29(x1181,x1182) % 116.67/116.73 [119]~P18(x1191,x1192)+P19(x1191,x1192) % 116.67/116.73 [120]~P18(x1201,x1202)+P13(x1201,x1202) % 116.67/116.73 [121]~P13(x1211,x1212)+P9(x1211,x1212) % 116.67/116.73 [122]~P13(x1221,x1222)+P14(x1221,x1222) % 116.67/116.73 [123]~P13(x1231,x1232)+P27(x1231,x1232) % 116.67/116.73 [124]~P27(x1241,x1242)+P20(x1241,x1242) % 116.67/116.73 [125]~P27(x1251,x1252)+P16(x1251,x1252) % 116.67/116.73 [126]~P27(x1261,x1262)+P10(x1261,x1262) % 116.67/116.73 [127]~P10(x1271,x1272)+P11(x1271,x1272) % 116.67/116.73 [128]~P10(x1281,x1282)+P30(x1281,x1282) % 116.67/116.73 [129]~P12(x1291,x1292)+P30(x1291,x1292) % 116.67/116.73 [130]~P10(x1301,x1302)+P35(x1301,x1302) % 116.67/116.73 [131]~P12(x1311,x1312)+P35(x1311,x1312) % 116.67/116.73 [132]~P3(x1321,x1322)+P35(x1321,x1322) % 116.67/116.73 [133]~P21(x1331,x1332)+P6(x1331,x1332) % 116.67/116.73 [134]~P31(x1341,x1342)+P6(x1341,x1342) % 116.67/116.73 [135]~P21(x1351,x1352)+P12(x1351,x1352) % 116.67/116.73 [136]~P6(x1361,x1362)+P12(x1361,x1362) % 116.67/116.73 [137]~P29(x1371,x1372)+P3(x1371,x1372) % 116.67/116.73 [138]~P12(x1381,x1382)+P36(x1381,x1382) % 116.67/116.73 [139]~P3(x1391,x1392)+P36(x1391,x1392) % 116.67/116.73 [140]~P3(x1401,x1402)+P15(x1401,x1402) % 116.67/116.73 [141]~P3(x1411,x1412)+P25(x1411,x1412) % 116.67/116.73 [142]~P12(x1421,x1422)+P26(x1421,x1422) % 116.67/116.73 [143]~P35(x1431,x1432)+P32(x1431,x1432) % 116.67/116.73 [147]~P36(x1471,x1472)+~P19(x1471,x1472) % 116.67/116.73 [148]~P25(x1481,x1482)+~P14(x1481,x1482) % 116.67/116.73 [149]~P26(x1491,x1492)+~P11(x1491,x1492) % 116.67/116.73 [150]~P15(x1501,x1502)+~P30(x1501,x1502) % 116.67/116.73 [186]E(x1861,x1862)+~P8(x1863,x1864,x1861,x1862) % 116.67/116.73 [151]~P2(x1513,x1511)+P4(x1511,x1512)+~P4(x1513,x1512) % 116.67/116.73 [152]~P2(x1523,x1521)+P5(x1521,x1522)+~P5(x1523,x1522) % 116.67/116.73 [153]~P2(x1533,x1531)+P17(x1531,x1532)+~P17(x1533,x1532) % 116.67/116.73 [154]~P2(x1543,x1541)+P28(x1541,x1542)+~P28(x1543,x1542) % 116.67/116.73 [155]~P2(x1553,x1551)+P29(x1551,x1552)+~P29(x1553,x1552) % 116.67/116.73 [156]~P2(x1563,x1561)+P18(x1561,x1562)+~P18(x1563,x1562) % 116.67/116.73 [157]~P2(x1573,x1571)+P19(x1571,x1572)+~P19(x1573,x1572) % 116.67/116.73 [158]~P2(x1583,x1581)+P13(x1581,x1582)+~P13(x1583,x1582) % 116.67/116.73 [159]~P2(x1593,x1591)+P9(x1591,x1592)+~P9(x1593,x1592) % 116.67/116.73 [160]~P2(x1603,x1601)+P14(x1601,x1602)+~P14(x1603,x1602) % 116.67/116.73 [161]~P2(x1613,x1611)+P27(x1611,x1612)+~P27(x1613,x1612) % 116.67/116.73 [162]~P2(x1623,x1621)+P20(x1621,x1622)+~P20(x1623,x1622) % 116.67/116.73 [163]~P2(x1633,x1631)+P16(x1631,x1632)+~P16(x1633,x1632) % 116.67/116.73 [164]~P2(x1643,x1641)+P10(x1641,x1642)+~P10(x1643,x1642) % 116.67/116.73 [165]~P2(x1653,x1651)+P11(x1651,x1652)+~P11(x1653,x1652) % 116.67/116.73 [166]~P2(x1663,x1661)+P30(x1661,x1662)+~P30(x1663,x1662) % 116.67/116.73 [167]~P2(x1673,x1671)+P35(x1671,x1672)+~P35(x1673,x1672) % 116.67/116.73 [168]~P2(x1683,x1681)+P21(x1681,x1682)+~P21(x1683,x1682) % 116.67/116.73 [169]~P2(x1693,x1691)+P6(x1691,x1692)+~P6(x1693,x1692) % 116.67/116.73 [170]~P2(x1703,x1701)+P12(x1701,x1702)+~P12(x1703,x1702) % 116.67/116.73 [171]~P2(x1713,x1711)+P3(x1711,x1712)+~P3(x1713,x1712) % 116.67/116.73 [172]~P2(x1723,x1721)+P36(x1721,x1722)+~P36(x1723,x1722) % 116.67/116.73 [173]~P2(x1733,x1731)+P15(x1731,x1732)+~P15(x1733,x1732) % 116.67/116.73 [174]~P2(x1743,x1741)+P25(x1741,x1742)+~P25(x1743,x1742) % 116.67/116.73 [175]~P2(x1753,x1751)+P22(x1751,x1752)+~P22(x1753,x1752) % 116.67/116.73 [176]~P2(x1763,x1761)+P26(x1761,x1762)+~P26(x1763,x1762) % 116.67/116.73 [177]~P2(x1773,x1771)+P32(x1771,x1772)+~P32(x1773,x1772) % 116.67/116.73 [178]~P2(x1783,x1781)+P31(x1781,x1782)+~P31(x1783,x1782) % 116.67/116.73 [179]~P33(x1793,x1792)+P33(x1791,x1792)+~P2(x1793,x1791) % 116.67/116.73 [180]~P23(x1803,x1802)+P23(x1801,x1802)+~P2(x1803,x1801) % 116.67/116.73 [182]~P24(x1824,x1822,x1823)+P24(x1821,x1822,x1823)+~P2(x1824,x1821) % 116.67/116.73 [183]~P34(x1834,x1832,x1833)+P34(x1831,x1832,x1833)+~P2(x1834,x1831) % 116.67/116.73 [184]~P7(x1844,x1842,x1843)+P7(x1841,x1842,x1843)+~P2(x1844,x1841) % 116.67/116.73 [188]~P8(x1885,x1882,x1883,x1884)+P8(x1881,x1882,x1883,x1884)+~P2(x1885,x1881) % 116.67/116.73 [185]~P5(x1853,x1851)+~P24(x1853,x1852,x1854)+~P24(x1853,x1851,x1854)+E(x1851,x1852)+~P5(x1853,x1852)+~P10(x1853,x1854) % 116.67/116.73 [187]~P22(x1873,x1871)+~P34(x1873,x1874,x1872)+~P34(x1873,x1875,x1871)+~P7(x1873,x1875,x1876)+E(x1871,x1872)+~P22(x1873,x1872)+~P33(x1873,x1874)+~P7(x1873,x1874,x1876)+~P33(x1873,x1875) % 116.67/116.73 [189]P18(x1891,f2(x1892,x1893,x1894,x1895,x1896,x1897,x1898,x1899,x1891,x18910,x18911,x18912,x18913,x18914))+~P1(x1892)+~P4(x1892,x18910)+~P4(x1892,x1896)+~P5(x1892,x18910)+~P5(x1892,x1898)+~P5(x1892,x1896)+~P5(x1892,x1894)+~P17(x1892,x1898)+~P17(x1892,x1894)+~P18(x1892,x18911)+~P18(x1892,x1897)+~P18(x1892,x1895)+~P18(x1892,x1893)+~P21(x1892,x18912)+~P6(x18914,x18915)+~P6(x1892,x18913)+~P6(x1892,x1899)+~P22(x1892,x18914)+~P22(x1892,x1891)+~P31(x18914,x18915)+~P2(x1892,x18914)+~P2(x1892,x1891)+~P33(x1892,x18913)+~P33(x1892,x1899)+~P23(x18914,x18915)+~P23(x1892,x18913)+~P23(x1892,x1899)+~P24(x1892,x18910,x18911)+~P24(x1892,x1898,x1897)+~P24(x1892,x1896,x1895)+~P24(x1892,x1894,x1893)+~P34(x1892,x18913,x18914)+~P34(x1892,x1899,x1891)+~P7(x18914,x18915,x1895)+~P7(x1892,x18913,x1893)+~P7(x1892,x1899,x1897)+~P8(x1892,x18912,x18911,x18911) % 116.67/116.73 [190]~P1(x1901)+~P4(x1901,x1902)+~P4(x1901,x1903)+~P5(x1901,x1902)+~P5(x1901,x1904)+~P5(x1901,x1903)+~P5(x1901,x1905)+~P17(x1901,x1904)+~P17(x1901,x1905)+~P18(x1901,x1906)+~P18(x1901,x1907)+~P18(x1901,x1908)+~P18(x1901,x1909)+~P21(x1901,x19010)+~P6(x19011,x19012)+~P6(x1901,x19013)+~P6(x1901,x19014)+~P6(x19015,x19016)+~P22(x1901,x19011)+~P22(x1901,x19015)+~P31(x19011,x19012)+~P31(x19015,x19016)+~P2(x1901,x19011)+~P2(x1901,x19015)+~P33(x1901,x19013)+~P33(x1901,x19014)+~P23(x19011,x19012)+~P23(x1901,x19013)+~P23(x1901,x19014)+~P23(x19015,x19016)+~P24(x1901,x1902,x1906)+~P24(x1901,x1904,x1907)+~P24(x1901,x1903,x1908)+~P24(x1901,x1905,x1909)+~P34(x1901,x19013,x19011)+~P34(x1901,x19014,x19015)+~P7(x19011,x19012,x1908)+~P7(x1901,x19013,x1909)+~P7(x1901,x19014,x1907)+~P8(x1901,x19010,x1906,x1906)+~P7(x19015,x19016,f2(x1901,x1909,x1905,x1908,x1903,x1907,x1904,x19014,x19015,x1902,x1906,x19010,x19013,x19011)) % 116.67/116.73 %EqnAxiom % 116.67/116.73 [1]E(x11,x11) % 116.67/116.73 [2]E(x22,x21)+~E(x21,x22) % 116.67/116.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.67/116.73 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 116.67/116.73 [5]~E(x51,x52)+E(f2(x51,x53,x54,x55,x56,x57,x58,x59,x510,x511,x512,x513,x514,x515),f2(x52,x53,x54,x55,x56,x57,x58,x59,x510,x511,x512,x513,x514,x515)) % 116.67/116.73 [6]~E(x61,x62)+E(f2(x63,x61,x64,x65,x66,x67,x68,x69,x610,x611,x612,x613,x614,x615),f2(x63,x62,x64,x65,x66,x67,x68,x69,x610,x611,x612,x613,x614,x615)) % 116.67/116.73 [7]~E(x71,x72)+E(f2(x73,x74,x71,x75,x76,x77,x78,x79,x710,x711,x712,x713,x714,x715),f2(x73,x74,x72,x75,x76,x77,x78,x79,x710,x711,x712,x713,x714,x715)) % 116.67/116.73 [8]~E(x81,x82)+E(f2(x83,x84,x85,x81,x86,x87,x88,x89,x810,x811,x812,x813,x814,x815),f2(x83,x84,x85,x82,x86,x87,x88,x89,x810,x811,x812,x813,x814,x815)) % 116.67/116.73 [9]~E(x91,x92)+E(f2(x93,x94,x95,x96,x91,x97,x98,x99,x910,x911,x912,x913,x914,x915),f2(x93,x94,x95,x96,x92,x97,x98,x99,x910,x911,x912,x913,x914,x915)) % 116.67/116.73 [10]~E(x101,x102)+E(f2(x103,x104,x105,x106,x107,x101,x108,x109,x1010,x1011,x1012,x1013,x1014,x1015),f2(x103,x104,x105,x106,x107,x102,x108,x109,x1010,x1011,x1012,x1013,x1014,x1015)) % 116.67/116.73 [11]~E(x111,x112)+E(f2(x113,x114,x115,x116,x117,x118,x111,x119,x1110,x1111,x1112,x1113,x1114,x1115),f2(x113,x114,x115,x116,x117,x118,x112,x119,x1110,x1111,x1112,x1113,x1114,x1115)) % 116.67/116.73 [12]~E(x121,x122)+E(f2(x123,x124,x125,x126,x127,x128,x129,x121,x1210,x1211,x1212,x1213,x1214,x1215),f2(x123,x124,x125,x126,x127,x128,x129,x122,x1210,x1211,x1212,x1213,x1214,x1215)) % 116.67/116.73 [13]~E(x131,x132)+E(f2(x133,x134,x135,x136,x137,x138,x139,x1310,x131,x1311,x1312,x1313,x1314,x1315),f2(x133,x134,x135,x136,x137,x138,x139,x1310,x132,x1311,x1312,x1313,x1314,x1315)) % 116.67/116.73 [14]~E(x141,x142)+E(f2(x143,x144,x145,x146,x147,x148,x149,x1410,x1411,x141,x1412,x1413,x1414,x1415),f2(x143,x144,x145,x146,x147,x148,x149,x1410,x1411,x142,x1412,x1413,x1414,x1415)) % 116.67/116.73 [15]~E(x151,x152)+E(f2(x153,x154,x155,x156,x157,x158,x159,x1510,x1511,x1512,x151,x1513,x1514,x1515),f2(x153,x154,x155,x156,x157,x158,x159,x1510,x1511,x1512,x152,x1513,x1514,x1515)) % 116.67/116.73 [16]~E(x161,x162)+E(f2(x163,x164,x165,x166,x167,x168,x169,x1610,x1611,x1612,x1613,x161,x1614,x1615),f2(x163,x164,x165,x166,x167,x168,x169,x1610,x1611,x1612,x1613,x162,x1614,x1615)) % 116.67/116.73 [17]~E(x171,x172)+E(f2(x173,x174,x175,x176,x177,x178,x179,x1710,x1711,x1712,x1713,x1714,x171,x1715),f2(x173,x174,x175,x176,x177,x178,x179,x1710,x1711,x1712,x1713,x1714,x172,x1715)) % 116.67/116.73 [18]~E(x181,x182)+E(f2(x183,x184,x185,x186,x187,x188,x189,x1810,x1811,x1812,x1813,x1814,x1815,x181),f2(x183,x184,x185,x186,x187,x188,x189,x1810,x1811,x1812,x1813,x1814,x1815,x182)) % 116.67/116.73 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 116.67/116.73 [20]P4(x202,x203)+~E(x201,x202)+~P4(x201,x203) % 116.67/116.73 [21]P4(x213,x212)+~E(x211,x212)+~P4(x213,x211) % 116.67/116.73 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223) % 116.67/116.73 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231) % 116.67/116.73 [24]P24(x242,x243,x244)+~E(x241,x242)+~P24(x241,x243,x244) % 116.67/116.73 [25]P24(x253,x252,x254)+~E(x251,x252)+~P24(x253,x251,x254) % 116.67/116.73 [26]P24(x263,x264,x262)+~E(x261,x262)+~P24(x263,x264,x261) % 116.67/116.73 [27]P17(x272,x273)+~E(x271,x272)+~P17(x271,x273) % 116.67/116.73 [28]P17(x283,x282)+~E(x281,x282)+~P17(x283,x281) % 116.67/116.73 [29]P18(x292,x293)+~E(x291,x292)+~P18(x291,x293) % 116.67/116.73 [30]P18(x303,x302)+~E(x301,x302)+~P18(x303,x301) % 116.67/116.73 [31]P34(x312,x313,x314)+~E(x311,x312)+~P34(x311,x313,x314) % 116.67/116.73 [32]P34(x323,x322,x324)+~E(x321,x322)+~P34(x323,x321,x324) % 116.67/116.73 [33]P34(x333,x334,x332)+~E(x331,x332)+~P34(x333,x334,x331) % 116.67/116.73 [34]P21(x342,x343)+~E(x341,x342)+~P21(x341,x343) % 116.67/116.73 [35]P21(x353,x352)+~E(x351,x352)+~P21(x353,x351) % 116.67/116.73 [36]P31(x362,x363)+~E(x361,x362)+~P31(x361,x363) % 116.67/116.73 [37]P31(x373,x372)+~E(x371,x372)+~P31(x373,x371) % 116.67/116.73 [38]P6(x382,x383)+~E(x381,x382)+~P6(x381,x383) % 116.67/116.73 [39]P6(x393,x392)+~E(x391,x392)+~P6(x393,x391) % 116.67/116.73 [40]P22(x402,x403)+~E(x401,x402)+~P22(x401,x403) % 116.67/116.73 [41]P22(x413,x412)+~E(x411,x412)+~P22(x413,x411) % 116.67/116.73 [42]P2(x422,x423)+~E(x421,x422)+~P2(x421,x423) % 116.67/116.73 [43]P2(x433,x432)+~E(x431,x432)+~P2(x433,x431) % 116.67/116.73 [44]P33(x442,x443)+~E(x441,x442)+~P33(x441,x443) % 116.67/116.73 [45]P33(x453,x452)+~E(x451,x452)+~P33(x453,x451) % 116.67/116.73 [46]P23(x462,x463)+~E(x461,x462)+~P23(x461,x463) % 116.67/116.73 [47]P23(x473,x472)+~E(x471,x472)+~P23(x473,x471) % 116.67/116.73 [48]P7(x482,x483,x484)+~E(x481,x482)+~P7(x481,x483,x484) % 116.67/116.73 [49]P7(x493,x492,x494)+~E(x491,x492)+~P7(x493,x491,x494) % 116.67/116.73 [50]P7(x503,x504,x502)+~E(x501,x502)+~P7(x503,x504,x501) % 116.67/116.73 [51]P20(x512,x513)+~E(x511,x512)+~P20(x511,x513) % 116.67/116.73 [52]P20(x523,x522)+~E(x521,x522)+~P20(x523,x521) % 116.67/116.73 [53]P13(x532,x533)+~E(x531,x532)+~P13(x531,x533) % 116.67/116.73 [54]P13(x543,x542)+~E(x541,x542)+~P13(x543,x541) % 116.67/116.73 [55]P36(x552,x553)+~E(x551,x552)+~P36(x551,x553) % 116.67/116.73 [56]P36(x563,x562)+~E(x561,x562)+~P36(x563,x561) % 116.67/116.73 [57]P8(x572,x573,x574,x575)+~E(x571,x572)+~P8(x571,x573,x574,x575) % 116.67/116.73 [58]P8(x583,x582,x584,x585)+~E(x581,x582)+~P8(x583,x581,x584,x585) % 116.67/116.73 [59]P8(x593,x594,x592,x595)+~E(x591,x592)+~P8(x593,x594,x591,x595) % 116.67/116.73 [60]P8(x603,x604,x605,x602)+~E(x601,x602)+~P8(x603,x604,x605,x601) % 116.67/116.73 [61]P12(x612,x613)+~E(x611,x612)+~P12(x611,x613) % 116.67/116.73 [62]P12(x623,x622)+~E(x621,x622)+~P12(x623,x621) % 116.67/116.73 [63]P27(x632,x633)+~E(x631,x632)+~P27(x631,x633) % 116.67/116.73 [64]P27(x643,x642)+~E(x641,x642)+~P27(x643,x641) % 116.67/116.73 [65]P11(x652,x653)+~E(x651,x652)+~P11(x651,x653) % 116.67/116.73 [66]P11(x663,x662)+~E(x661,x662)+~P11(x663,x661) % 116.67/116.73 [67]P15(x672,x673)+~E(x671,x672)+~P15(x671,x673) % 116.67/116.73 [68]P15(x683,x682)+~E(x681,x682)+~P15(x683,x681) % 116.67/116.73 [69]P28(x692,x693)+~E(x691,x692)+~P28(x691,x693) % 116.67/116.73 [70]P28(x703,x702)+~E(x701,x702)+~P28(x703,x701) % 116.67/116.73 [71]P14(x712,x713)+~E(x711,x712)+~P14(x711,x713) % 116.67/116.73 [72]P14(x723,x722)+~E(x721,x722)+~P14(x723,x721) % 116.67/116.73 [73]P29(x732,x733)+~E(x731,x732)+~P29(x731,x733) % 116.67/116.73 [74]P29(x743,x742)+~E(x741,x742)+~P29(x743,x741) % 116.67/116.73 [75]P26(x752,x753)+~E(x751,x752)+~P26(x751,x753) % 116.67/116.73 [76]P26(x763,x762)+~E(x761,x762)+~P26(x763,x761) % 116.67/116.73 [77]P10(x772,x773)+~E(x771,x772)+~P10(x771,x773) % 116.67/116.73 [78]P10(x783,x782)+~E(x781,x782)+~P10(x783,x781) % 116.67/116.73 [79]P16(x792,x793)+~E(x791,x792)+~P16(x791,x793) % 116.67/116.73 [80]P16(x803,x802)+~E(x801,x802)+~P16(x803,x801) % 116.67/116.73 [81]P19(x812,x813)+~E(x811,x812)+~P19(x811,x813) % 116.67/116.73 [82]P19(x823,x822)+~E(x821,x822)+~P19(x823,x821) % 116.67/116.73 [83]P30(x832,x833)+~E(x831,x832)+~P30(x831,x833) % 116.67/116.73 [84]P30(x843,x842)+~E(x841,x842)+~P30(x843,x841) % 116.67/116.73 [85]P25(x852,x853)+~E(x851,x852)+~P25(x851,x853) % 116.67/116.73 [86]P25(x863,x862)+~E(x861,x862)+~P25(x863,x861) % 116.67/116.73 [87]P3(x872,x873)+~E(x871,x872)+~P3(x871,x873) % 116.67/116.73 [88]P3(x883,x882)+~E(x881,x882)+~P3(x883,x881) % 116.67/116.73 [89]P9(x892,x893)+~E(x891,x892)+~P9(x891,x893) % 116.67/116.73 [90]P9(x903,x902)+~E(x901,x902)+~P9(x903,x901) % 116.67/116.73 [91]P35(x912,x913)+~E(x911,x912)+~P35(x911,x913) % 116.67/116.73 [92]P35(x923,x922)+~E(x921,x922)+~P35(x923,x921) % 116.67/116.73 [93]P32(x932,x933)+~E(x931,x932)+~P32(x931,x933) % 116.67/116.74 [94]P32(x943,x942)+~E(x941,x942)+~P32(x943,x941) % 116.67/116.74 % 116.67/116.74 %------------------------------------------- % 116.67/116.74 cnf(193,plain, % 116.67/116.74 (P5(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[96,97,106,151,152])). % 116.67/116.74 cnf(197,plain, % 116.67/116.74 (P18(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[96,97,99,100,106,151,152,153,156])). % 116.67/116.74 cnf(199,plain, % 116.67/116.74 (P21(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[96,97,99,100,103,106,151,152,153,156,168])). % 116.67/116.74 cnf(201,plain, % 116.67/116.74 (P6(a7,a6)), % 116.67/116.74 inference(scs_inference,[],[96,97,99,100,103,104,106,151,152,153,156,168,169])). % 116.67/116.74 cnf(209,plain, % 116.67/116.74 (P24(a7,a4,a5)), % 116.67/116.74 inference(scs_inference,[],[96,97,99,100,103,104,105,106,107,108,109,151,152,153,156,168,169,175,179,180,182])). % 116.67/116.74 cnf(229,plain, % 116.67/116.74 (P18(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[102,106,156])). % 116.67/116.74 cnf(236,plain, % 116.67/116.74 (P18(a1,x2361)+~E(a8,x2361)), % 116.67/116.74 inference(scs_inference,[],[98,102,110,106,156,152,182,29,30])). % 116.67/116.74 cnf(375,plain, % 116.67/116.74 (P21(a7,x3751)+~E(a9,x3751)), % 116.67/116.74 inference(scs_inference,[],[199,35])). % 116.67/116.74 cnf(380,plain, % 116.67/116.74 (P6(a7,x3801)+~E(a6,x3801)), % 116.67/116.74 inference(scs_inference,[],[201,209,26,39])). % 116.67/116.74 cnf(420,plain, % 116.67/116.74 (P28(a1,a3)), % 116.67/116.74 inference(scs_inference,[],[96,114,116])). % 116.67/116.74 cnf(421,plain, % 116.67/116.74 (P28(a7,a3)), % 116.67/116.74 inference(scs_inference,[],[106,420,154])). % 116.67/116.74 cnf(450,plain, % 116.67/116.74 (P28(a1,a4)), % 116.67/116.74 inference(scs_inference,[],[99,115,116])). % 116.67/116.74 cnf(451,plain, % 116.67/116.74 (P28(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[106,450,154])). % 116.67/116.74 cnf(480,plain, % 116.67/116.74 (P3(a7,a3)), % 116.67/116.74 inference(scs_inference,[],[421,117,137])). % 116.67/116.74 cnf(503,plain, % 116.67/116.74 (P3(a1,a7)), % 116.67/116.74 inference(scs_inference,[],[105,118,137])). % 116.67/116.74 cnf(504,plain, % 116.67/116.74 (P3(a7,a7)), % 116.67/116.74 inference(scs_inference,[],[106,503,171])). % 116.67/116.74 cnf(515,plain, % 116.67/116.74 (P3(a7,x5151)+~E(a7,x5151)), % 116.67/116.74 inference(scs_inference,[],[504,171,87,88])). % 116.67/116.74 cnf(533,plain, % 116.67/116.74 (~P36(a1,a8)), % 116.67/116.74 inference(scs_inference,[],[102,119,147])). % 116.67/116.74 cnf(547,plain, % 116.67/116.74 (~P8(x5471,x5472,a7,a8)), % 116.67/116.74 inference(scs_inference,[],[503,533,138,139,88,135,136,134,137,186])). % 116.67/116.74 cnf(638,plain, % 116.67/116.74 (~P13(x6381,x6382)+~P25(x6381,x6382)), % 116.67/116.74 inference(scs_inference,[],[122,148])). % 116.67/116.74 cnf(686,plain, % 116.67/116.74 (P11(x6861,x6862)+~P27(x6861,x6862)), % 116.67/116.74 inference(scs_inference,[],[126,127])). % 116.67/116.74 cnf(702,plain, % 116.67/116.74 (~P10(x7021,x7022)+~P15(x7021,x7022)), % 116.67/116.74 inference(scs_inference,[],[128,150])). % 116.67/116.74 cnf(718,plain, % 116.67/116.74 (~P12(x7181,x7182)+~P15(x7181,x7182)), % 116.67/116.74 inference(scs_inference,[],[129,150])). % 116.67/116.74 cnf(750,plain, % 116.67/116.74 (P32(x7501,x7502)+~P12(x7501,x7502)), % 116.67/116.74 inference(scs_inference,[],[131,143])). % 116.67/116.74 cnf(789,plain, % 116.67/116.74 (P12(a1,a9)), % 116.67/116.74 inference(scs_inference,[],[103,133,136])). % 116.67/116.74 cnf(792,plain, % 116.67/116.74 (P12(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[106,789,750,170])). % 116.67/116.74 cnf(860,plain, % 116.67/116.74 (~P14(a7,a7)), % 116.67/116.74 inference(scs_inference,[],[504,141,148])). % 116.67/116.74 cnf(876,plain, % 116.67/116.74 (~P11(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[792,142,149])). % 116.67/116.74 cnf(1129,plain, % 116.67/116.74 (~P25(a1,x11291)+~P13(a7,x11291)), % 116.67/116.74 inference(scs_inference,[],[106,638,174])). % 116.67/116.74 cnf(1215,plain, % 116.67/116.74 (~P3(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[792,718,140])). % 116.67/116.74 cnf(1223,plain, % 116.67/116.74 (~P22(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[504,1215,137,88,117,116,118])). % 116.67/116.74 cnf(1231,plain, % 116.67/116.74 (~P4(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[112,111,105,107,504,193,421,1215,137,88,117,116,118,186,70,23,187,114])). % 116.67/116.74 cnf(1233,plain, % 116.67/116.74 (~P17(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[112,111,105,107,504,193,421,1215,137,88,117,116,118,186,70,23,187,114,115])). % 116.67/116.74 cnf(1736,plain, % 116.67/116.74 (P23(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[100,106,146,156])). % 116.67/116.74 cnf(1903,plain, % 116.67/116.74 (P7(a7,f10(a8),a8)), % 116.67/116.74 inference(scs_inference,[],[102,106,181,156])). % 116.67/116.74 cnf(1904,plain, % 116.67/116.74 (P7(a7,x19041,a8)+~E(f10(a8),x19041)), % 116.67/116.74 inference(scs_inference,[],[1903,49])). % 116.67/116.74 cnf(2856,plain, % 116.67/116.74 (P31(x28561,f10(a5))+~E(a7,x28561)), % 116.67/116.74 inference(scs_inference,[],[197,36,145])). % 116.67/116.74 cnf(2857,plain, % 116.67/116.74 (P31(a7,f10(a5))), % 116.67/116.74 inference(equality_inference,[],[2856])). % 116.67/116.74 cnf(2866,plain, % 116.67/116.74 (P31(a7,x28661)+~E(f10(a5),x28661)), % 116.67/116.74 inference(scs_inference,[],[2857,37])). % 116.67/116.74 cnf(3388,plain, % 116.67/116.74 (~P27(a7,x33881)+~E(x33881,a9)), % 116.67/116.74 inference(scs_inference,[],[876,66,686])). % 116.67/116.74 cnf(3405,plain, % 116.67/116.74 (~P15(a1,x34051)+P15(x34052,x34051)+~E(a7,x34052)), % 116.67/116.74 inference(scs_inference,[],[106,67,173])). % 116.67/116.74 cnf(3406,plain, % 116.67/116.74 (P15(a7,x34061)+~P15(a1,x34061)), % 116.67/116.74 inference(equality_inference,[],[3405])). % 116.67/116.74 cnf(3422,plain, % 116.67/116.74 (P15(a7,a7)), % 116.67/116.74 inference(scs_inference,[],[503,3406,140])). % 116.67/116.74 cnf(3427,plain, % 116.67/116.74 (~P6(a7,a7)), % 116.67/116.74 inference(scs_inference,[],[3422,718,135,136])). % 116.67/116.74 cnf(3930,plain, % 116.67/116.74 (~P13(a7,x39301)+~E(x39301,a7)), % 116.67/116.74 inference(scs_inference,[],[860,72,122])). % 116.67/116.74 cnf(3981,plain, % 116.67/116.74 (~P26(a1,x39811)+P26(x39812,x39811)+~E(a7,x39812)), % 116.67/116.74 inference(scs_inference,[],[106,75,176])). % 116.67/116.74 cnf(3982,plain, % 116.67/116.74 (P26(a7,x39821)+~P26(a1,x39821)), % 116.67/116.74 inference(equality_inference,[],[3981])). % 116.67/116.74 cnf(4122,plain, % 116.67/116.74 (~P19(a1,x41221)+P19(a7,x41222)+~E(x41221,x41222)), % 116.67/116.74 inference(scs_inference,[],[106,82,157])). % 116.67/116.74 cnf(4123,plain, % 116.67/116.74 (~P19(a1,x41231)+P19(a7,x41231)), % 116.67/116.74 inference(equality_inference,[],[4122])). % 116.67/116.74 cnf(4139,plain, % 116.67/116.74 (P19(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[100,4123,119])). % 116.67/116.74 cnf(4140,plain, % 116.67/116.74 (~P36(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147])). % 116.67/116.74 cnf(4142,plain, % 116.67/116.74 (~P3(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139])). % 116.67/116.74 cnf(4144,plain, % 116.67/116.74 (~P12(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138])). % 116.67/116.74 cnf(4146,plain, % 116.67/116.74 (~P6(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136])). % 116.67/116.74 cnf(4150,plain, % 116.67/116.74 (~P31(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134])). % 116.67/116.74 cnf(4152,plain, % 116.67/116.74 (~P29(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137])). % 116.67/116.74 cnf(4157,plain, % 116.67/116.74 (~P28(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137,2866,186,117])). % 116.67/116.74 cnf(4159,plain, % 116.67/116.74 (~P5(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137,2866,186,117,116])). % 116.67/116.74 cnf(4161,plain, % 116.67/116.74 (~P22(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137,2866,186,117,116,118])). % 116.67/116.74 cnf(4165,plain, % 116.67/116.74 (~P17(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137,2866,186,117,116,118,157,115])). % 116.67/116.74 cnf(4167,plain, % 116.67/116.74 (~P4(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[4139,147,139,138,136,135,134,137,2866,186,117,116,118,157,115,114])). % 116.67/116.74 cnf(4245,plain, % 116.67/116.74 (~P30(a1,x42451)+P30(x42452,x42451)+~E(a7,x42452)), % 116.67/116.74 inference(scs_inference,[],[106,83,166])). % 116.67/116.74 cnf(4246,plain, % 116.67/116.74 (P30(a7,x42461)+~P30(a1,x42461)), % 116.67/116.74 inference(equality_inference,[],[4245])). % 116.67/116.74 cnf(4262,plain, % 116.67/116.74 (P30(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[789,4246,129])). % 116.67/116.74 cnf(4263,plain, % 116.67/116.74 (~P15(a7,a9)), % 116.67/116.74 inference(scs_inference,[],[4262,150])). % 116.67/116.74 cnf(4399,plain, % 116.67/116.74 (P12(a1,a6)), % 116.67/116.74 inference(scs_inference,[],[104,136])). % 116.67/116.74 cnf(4401,plain, % 116.67/116.74 (P6(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[104,2857,136,134])). % 116.67/116.74 cnf(4403,plain, % 116.67/116.74 (P12(a7,a6)), % 116.67/116.74 inference(scs_inference,[],[106,104,2857,136,134,170])). % 116.67/116.74 cnf(4419,plain, % 116.67/116.74 (P12(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[4401,136])). % 116.67/116.74 cnf(4447,plain, % 116.67/116.74 (P36(a1,a7)), % 116.67/116.74 inference(scs_inference,[],[503,139])). % 116.67/116.74 cnf(4459,plain, % 116.67/116.74 (P36(a7,a3)), % 116.67/116.74 inference(scs_inference,[],[451,480,117,139])). % 116.67/116.74 cnf(4461,plain, % 116.67/116.74 (P3(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[451,480,117,139,137])). % 116.67/116.74 cnf(4484,plain, % 116.67/116.74 (P36(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[105,420,4447,4461,147,118,117,139])). % 116.67/116.74 cnf(4486,plain, % 116.67/116.74 (P3(a1,a3)), % 116.67/116.74 inference(scs_inference,[],[105,420,4447,4461,147,118,117,139,137])). % 116.67/116.74 cnf(4513,plain, % 116.67/116.74 (P3(a1,a4)), % 116.67/116.74 inference(scs_inference,[],[789,450,4459,4486,138,147,139,117,137])). % 116.67/116.74 cnf(4532,plain, % 116.67/116.74 (P36(a1,a6)), % 116.67/116.74 inference(scs_inference,[],[4399,138])). % 116.67/116.74 cnf(4538,plain, % 116.67/116.74 (P36(a7,a6)), % 116.67/116.74 inference(scs_inference,[],[106,4399,4484,4513,138,147,139,172])). % 116.67/116.74 cnf(4557,plain, % 116.67/116.74 (P36(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[4419,138])). % 116.67/116.74 cnf(4577,plain, % 116.67/116.74 (~P30(a1,a7)), % 116.67/116.74 inference(scs_inference,[],[106,3422,4532,150,147,166])). % 116.67/116.74 cnf(4581,plain, % 116.67/116.74 (~P12(a1,a7)), % 116.67/116.74 inference(scs_inference,[],[106,3422,4532,150,147,166,128,129])). % 116.67/116.74 cnf(4599,plain, % 116.67/116.74 (~P19(a7,a6)), % 116.67/116.74 inference(scs_inference,[],[4538,147])). % 116.67/116.74 cnf(4603,plain, % 116.67/116.74 (P30(a1,a9)), % 116.67/116.74 inference(scs_inference,[],[106,789,1223,4538,147,175,129])). % 116.67/116.74 cnf(4611,plain, % 116.67/116.74 (~P3(a1,a9)), % 116.67/116.74 inference(scs_inference,[],[106,789,1223,4577,4263,4538,147,175,129,119,166,173,140])). % 116.67/116.74 cnf(4630,plain, % 116.67/116.74 (~P18(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[106,4399,4161,4557,129,147,175,157,4246,119])). % 116.67/116.74 cnf(4633,plain, % 116.67/116.74 (~P18(a1,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[106,4399,4161,4557,4603,129,147,175,157,4246,119,83,156])). % 116.67/116.74 cnf(4644,plain, % 116.67/116.74 (P30(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[4419,129])). % 116.67/116.74 cnf(5777,plain, % 116.67/116.74 (~P14(x57771,a7)+~E(x57771,a1)), % 116.67/116.74 inference(scs_inference,[],[106,860,160,71])). % 116.67/116.74 cnf(5778,plain, % 116.67/116.74 (~P14(a1,a7)), % 116.67/116.74 inference(equality_inference,[],[5777])). % 116.67/116.74 cnf(5880,plain, % 116.67/116.74 (P6(a7,f10(a8))), % 116.67/116.74 inference(scs_inference,[],[4633,4403,229,142,236,144])). % 116.67/116.74 cnf(5882,plain, % 116.67/116.74 (P31(a7,f10(a8))), % 116.67/116.74 inference(scs_inference,[],[4633,4403,229,142,236,144,145])). % 116.67/116.74 cnf(5884,plain, % 116.67/116.74 (P23(a7,f10(a8))), % 116.67/116.74 inference(scs_inference,[],[4633,4403,229,142,236,144,145,146])). % 116.67/116.74 cnf(5886,plain, % 116.67/116.74 (P7(a7,f10(a5),a5)), % 116.67/116.74 inference(scs_inference,[],[4633,4403,229,197,142,236,144,145,146,181])). % 116.67/116.74 cnf(5890,plain, % 116.67/116.74 (P15(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[4633,4403,4461,229,197,142,236,144,145,146,181,141,140])). % 116.67/116.74 cnf(5892,plain, % 116.67/116.74 (~P15(a7,a6)), % 116.67/116.74 inference(scs_inference,[],[4633,4403,4461,229,197,142,236,144,145,146,181,141,140,718])). % 116.67/116.74 cnf(5894,plain, % 116.67/116.74 (~P15(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[4633,4644,4403,4461,229,197,142,236,144,145,146,181,141,140,718,150])). % 116.67/116.74 cnf(5938,plain, % 116.67/116.74 (~P12(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[1233,4611,1231,4142,4157,4152,4581,4146,4150,4144,4159,4633,4644,4403,4461,4140,876,229,197,106,142,236,144,145,146,181,141,140,718,150,136,134,137,120,119,165,155,154,151,172,153,178,171,169,152,170,638,3406,122,133,147,138])). % 116.67/116.74 cnf(5948,plain, % 116.67/116.74 (P16(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[1233,4611,5778,1231,4142,4157,4152,4581,4146,4150,4144,4159,4633,4644,4403,4461,4140,876,229,197,106,142,236,144,145,146,181,141,140,718,150,136,134,137,120,119,165,155,154,151,172,153,178,171,169,152,170,638,3406,122,133,147,138,123,126,117,160,125])). % 116.67/116.74 cnf(5952,plain, % 116.67/116.74 (P11(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[1233,4611,5778,1231,4142,4157,4152,4581,4146,4150,4144,4159,4633,4644,4403,4461,4140,876,229,197,106,142,236,144,145,146,181,141,140,718,150,136,134,137,120,119,165,155,154,151,172,153,178,171,169,152,170,638,3406,122,133,147,138,123,126,117,160,125,130,686])). % 116.67/116.74 cnf(5956,plain, % 116.67/116.74 (~P3(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[1233,4611,5778,1231,4142,4157,4152,4581,4146,4150,4144,4159,4633,4644,4403,4461,4140,876,229,197,106,142,236,144,145,146,181,141,140,718,150,136,134,137,120,119,165,155,154,151,172,153,178,171,169,152,170,638,3406,122,133,147,138,123,126,117,160,125,130,686,128,139])). % 116.67/116.74 cnf(5958,plain, % 116.67/116.74 (~P15(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[1233,4611,5778,1231,4142,4157,4152,4581,4146,4150,4144,4159,4633,4644,4403,4461,4140,876,229,197,106,142,236,144,145,146,181,141,140,718,150,136,134,137,120,119,165,155,154,151,172,153,178,171,169,152,170,638,3406,122,133,147,138,123,126,117,160,125,130,686,128,139,702])). % 116.67/116.74 cnf(5975,plain, % 116.67/116.74 (~P6(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[5938,5952,5958,4513,4399,149,141,142,140,3406,136])). % 116.67/116.74 cnf(5979,plain, % 116.67/116.74 (~P29(a7,a8)), % 116.67/116.74 inference(scs_inference,[],[5938,5952,5956,5958,4513,4399,149,141,142,140,3406,136,134,137])). % 116.67/116.74 cnf(5981,plain, % 116.67/116.74 (P13(a7,a5)), % 116.67/116.74 inference(scs_inference,[],[5938,5952,5956,5958,4513,4399,197,149,141,142,140,3406,136,134,137,120])). % 116.67/116.74 cnf(5992,plain, % 116.67/116.74 (~P7(a7,f10(a8),f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[95,5892,5890,5938,5952,5956,5958,5880,5882,5884,4165,4167,3427,4150,4513,1903,4399,108,99,197,96,103,104,113,100,102,105,111,106,98,110,109,97,112,107,149,141,142,140,3406,136,134,137,120,119,39,153,68,151,37,190])). % 116.67/116.74 cnf(5994,plain, % 116.67/116.74 (~P13(a7,a4)), % 116.67/116.74 inference(scs_inference,[],[95,5892,5890,5938,5952,5956,5958,5880,5882,5884,4165,4167,3427,4150,4513,1903,4399,108,99,197,96,103,104,113,100,102,105,111,106,98,110,109,97,112,107,149,141,142,140,3406,136,134,137,120,119,39,153,68,151,37,190,1129])). % 116.67/116.74 cnf(6001,plain, % 116.67/116.74 (P25(a1,a3)), % 116.67/116.74 inference(scs_inference,[],[5975,4486,133,141])). % 116.67/116.74 cnf(6011,plain, % 116.67/116.74 (P26(a7,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[5975,5981,5894,4486,4419,133,141,122,1129,638,3406,142])). % 116.67/116.74 cnf(6047,plain, % 116.67/116.74 (P15(a7,a3)), % 116.67/116.74 inference(scs_inference,[],[5948,5975,5979,5981,5894,5992,4486,4419,102,106,133,141,122,1129,638,3406,142,140,118,123,117,126,119,120,184,686,130,149,128,125,150,116,163,174,173])). % 116.67/116.74 cnf(6153,plain, % 116.67/116.74 (~E(a3,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[6047,5894,68])). % 116.67/116.74 cnf(6801,plain, % 116.67/116.74 (P18(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189])). % 116.67/116.74 cnf(6803,plain, % 116.67/116.74 (P19(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119])). % 116.67/116.74 cnf(6805,plain, % 116.67/116.74 (P13(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120])). % 116.67/116.74 cnf(6809,plain, % 116.67/116.74 (~P36(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147])). % 116.67/116.74 cnf(6814,plain, % 116.67/116.74 (~P12(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138])). % 116.67/116.74 cnf(6816,plain, % 116.67/116.74 (P27(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123])). % 116.67/116.74 cnf(6818,plain, % 116.67/116.74 (~P6(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136])). % 116.67/116.74 cnf(6820,plain, % 116.67/116.74 (~P31(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134])). % 116.67/116.74 cnf(6822,plain, % 116.67/116.74 (~P21(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134,133])). % 116.67/116.74 cnf(6826,plain, % 116.67/116.74 (~P3(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134,133,122,139])). % 116.67/116.74 cnf(6828,plain, % 116.67/116.74 (P10(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134,133,122,139,126])). % 116.67/116.74 cnf(6834,plain, % 116.67/116.74 (P11(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134,133,122,139,126,128,125,686])). % 116.67/116.74 cnf(6836,plain, % 116.67/116.74 (~P15(a7,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[103,547,1903,99,5880,5884,108,5882,95,96,104,100,113,102,111,105,112,107,106,110,98,109,97,189,119,120,638,147,60,3930,138,123,136,134,133,122,139,126,128,125,686,150])). % 116.67/116.74 cnf(6885,plain, % 116.67/116.74 (~P5(a1,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[6809,6803,6805,6814,6816,6818,6820,6822,6826,6828,6834,6836,6801,4630,5994,4599,2857,106,193,375,380,515,3388,137,149,130,3406,117,116,118,23,171,178,155,168,170,172,169,3982,54,40,37,82,154,30,152])). % 116.67/116.74 cnf(6915,plain, % 116.67/116.74 (~E(f10(a8),f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[6820,5882,37])). % 116.67/116.74 cnf(7112,plain, % 116.67/116.74 (~P7(a7,f10(a5),f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[108,1903,99,4401,1736,5884,95,5880,103,96,2857,5882,113,104,100,102,111,105,112,107,106,110,98,109,97,190])). % 116.67/116.74 cnf(7120,plain, % 116.67/116.74 (~P7(a7,x71201,f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))+~E(x71201,f10(a5))), % 116.67/116.74 inference(scs_inference,[],[7112,5886,106,184,50,49])). % 116.67/116.74 cnf(7941,plain, % 116.67/116.74 (~P10(a7,a3)), % 116.67/116.74 inference(scs_inference,[],[6047,702])). % 116.67/116.74 cnf(7947,plain, % 116.67/116.74 (~P10(a1,a3)), % 116.67/116.74 inference(scs_inference,[],[7941,106,164])). % 116.67/116.74 cnf(8076,plain, % 116.67/116.74 (P23(a7,f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.67/116.74 inference(scs_inference,[],[6801,146])). % 116.67/116.74 cnf(8078,plain, % 116.67/116.74 (P7(a7,f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)),f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7))), % 116.67/116.74 inference(scs_inference,[],[6801,146,181])). % 116.67/116.74 cnf(8080,plain, % 116.67/116.74 (P6(a7,f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.67/116.74 inference(scs_inference,[],[6801,146,181,144])). % 116.67/116.74 cnf(8082,plain, % 116.67/116.74 (P31(a7,f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)))), % 116.67/116.74 inference(scs_inference,[],[6801,146,181,144,145])). % 116.67/116.74 cnf(8085,plain, % 116.67/116.74 (~E(f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)),f10(a5))), % 116.67/116.74 inference(scs_inference,[],[5992,6801,146,181,144,145,49,7120])). % 116.67/116.74 cnf(8095,plain, % 116.67/116.74 (~P7(a7,f10(f2(a1,a5,a4,a8,a3,a5,a4,a6,a7,a3,a8,a9,a6,a7)),a8)), % 116.67/116.74 inference(scs_inference,[],[8076,8078,8080,8082,100,102,107,106,109,110,113,98,97,95,103,104,99,96,112,105,108,111,190])). % 116.67/116.74 cnf(8139,plain, % 116.67/116.74 ($false), % 116.67/116.74 inference(scs_inference,[],[95,111,105,108,112,96,5884,99,104,5880,103,5882,97,98,113,110,109,1903,106,107,102,100,8082,8080,6153,6805,5890,8078,6820,5894,8076,6915,6885,6001,7947,6011,8095,8085,150,4,186,126,2,140,115,136,149,114,138,121,1904,148,37,166,190]), % 116.67/116.74 ['proof']). % 116.67/116.74 % SZS output end Proof % 116.67/116.74 % Total time :116.070000s %------------------------------------------------------------------------------