%------------------------------------------------------------------------------ % File : iProver---3.9.4 % Problem : NLP008-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % Computer : n012.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 : Fri Sep 25 02:16:12 PM UTC 2026 % Result : Satisfiable 0.45s 0.98s % Output : Model 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NLP008-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % 0.03/0.29 % Computer : n012.cluster.edu % 0.03/0.29 % Model : x86_64 x86_64 % 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.29 % Memory : 8046.5625MB % 0.03/0.29 % OS : Linux 6.8.0-71-generic % 0.03/0.29 % CPULimit : 300 % 0.03/0.29 % WCLimit : 300 % 0.03/0.29 % DateTime : Thu Sep 24 01:37:35 UTC 2026 % 0.03/0.29 % CPUTime : % 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM % 0.03/0.32 Running EPR theorem proving % 0.03/0.32 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.03/0.32 % 0.03/0.32 % ======== iProver multi-core TPTP/SMT ========= % 0.03/0.32 % 0.03/0.32 % Detected problem language: tptp % 0.03/0.33 % Proving... % 0.45/0.98 % SZS status Started for theBenchmark.p % 0.45/0.98 % SZS status Satisfiable for theBenchmark.p % 0.45/0.98 % 0.45/0.98 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------% % 0.45/0.98 % 0.45/0.98 % ------ iProver source info % 0.45/0.98 % 0.45/0.98 % git: date: 2026-07-19 20:42:38 +0200 % 0.45/0.98 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61 % 0.45/0.98 % git: non_committed_changes: false % 0.45/0.98 % 0.45/0.98 % ------ Parsing...% successful % 0.45/0.98 % 0.45/0.98 % 0.45/0.98 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_eq % 0.45/0.98 % % 0.45/0.98 % 0.45/0.98 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 14 0s sf_e pe_s pe_e % % 0.45/0.98 % 0.45/0.98 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_eq % 0.45/0.98 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Option_epr_non_horn_eq % 0.45/0.98 % % 0.45/0.98 % 0.45/0.98 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e % 0.45/0.98 % ------ Proving... % 0.45/0.98 % ------ Problem Properties % 0.45/0.98 % 0.45/0.98 % % 0.45/0.98 % clauses 31 % 0.45/0.98 % conjectures 29 % 0.45/0.98 % EPR 31 % 0.45/0.98 % Horn 21 % 0.45/0.98 % unary 7 % 0.45/0.98 % binary 22 % 0.45/0.98 % lits 80 % 0.45/0.98 % lits eq 4 % 0.45/0.98 % fd_pure 0 % 0.45/0.98 % fd_pseudo 0 % 0.45/0.98 % fd_cond 0 % 0.45/0.98 % fd_pseudo_cond 2 % 0.45/0.98 % AC symbols 0 % 0.45/0.98 % 0.45/0.98 % ------ Schedule EPR non Horn eq is on % 0.45/0.98 % 0.45/0.98 % ------ Option_epr_non_horn_eq Time Limit: Unbounded % 0.45/0.98 % 0.45/0.98 % 0.45/0.98 % ------ % 0.45/0.98 % Current options: % 0.45/0.98 % ------ % 0.45/0.98 % 0.45/0.98 % 0.45/0.98 % % 0.45/0.98 % 0.45/0.98 % ------ Proving... % 0.45/0.98 % % 0.45/0.98 % 0.45/0.98 % SZS status Satisfiable for theBenchmark.p % 0.45/0.98 % 0.45/0.98 ------ Building Model...Done % 0.45/0.98 % 0.45/0.98 %------ The model is defined over ground terms (initial term algebra). % 0.45/0.98 %------ Predicates are defined as (\forall x_1,..,x_n ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n)))) % 0.45/0.98 %------ where \phi is a formula over the term algebra. % 0.45/0.98 %------ If we have equality in the problem then it is also defined as a predicate above, % 0.45/0.98 %------ with "=" on the right-hand-side of the definition interpreted over the term algebra term_algebra_type % 0.45/0.98 %------ See help for --sat_out_model for different model outputs. % 0.45/0.98 %------ equality_sorted(X0,X1,X2) can be used in the place of usual "=" % 0.45/0.98 %------ where the first argument stands for the sort ($i in the unsorted case) % 0.45/0.98 % SZS output start Model for theBenchmark.p % 0.45/0.98 % 0.45/0.98 %------ Positive definition of equality_sorted % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_tType,X0_o,X1_o] : % 0.45/0.98 ( equality_sorted(X0_tType,X0_o,X1_o) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=$o & X1_o=X0_o ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=iProver_young_1 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc21 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc21 | X1_iProver_young_1!=skc15 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc16 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc16 | X1_iProver_young_1!=skc15 ) % 0.45/0.98 & % 0.45/0.98 ( X1_iProver_young_1!=skc21 ) % 0.45/0.98 & % 0.45/0.98 ( X1_iProver_young_1!=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=iProver_young_1 & X0_iProver_young_1=skc21 & X1_iProver_young_1=skc21 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=iProver_young_1 & X0_iProver_young_1=skc16 & X1_iProver_young_1=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=iProver_young_1 & X1_iProver_young_1=skc15 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc21 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_tType=iProver_young_1 & X1_iProver_young_1=X0_iProver_young_1 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc21 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of city % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( city(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of event % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( event(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of lonely % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( lonely(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of chevy % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( chevy(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of seat % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_seat_1] : % 0.45/0.98 ( seat(X0_iProver_seat_1) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc25 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc18 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc17 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of young % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_young_1] : % 0.45/0.98 ( young(X0_iProver_young_1) <=> % 0.45/0.98 $true % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of fellow % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_young_1] : % 0.45/0.98 ( fellow(X0_iProver_young_1) <=> % 0.45/0.98 $true % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of old % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( old(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of street % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( street(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of front % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_seat_1] : % 0.45/0.98 ( front(X0_iProver_seat_1) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc18 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc17 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of ssSkC0 % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 ( ssSkC0 <=> % 0.45/0.98 $true % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of dirty % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( dirty(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of white % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( white(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of car % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( car(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of way % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( way(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of hollywood % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0] : % 0.45/0.98 ( hollywood(X0) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of man % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_young_1] : % 0.45/0.98 ( man(X0_iProver_young_1) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1!=skc21 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1=skc15 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of furniture % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_seat_1] : % 0.45/0.98 ( furniture(X0_iProver_seat_1) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc18 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc17 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of down % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0,X1] : % 0.45/0.98 ( down(X0,X1) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of barrel % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0,X1] : % 0.45/0.98 ( barrel(X0,X1) <=> % 0.45/0.98 $false % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % 0.45/0.98 %------ Positive definition of in % 0.45/0.98 fof(lit_def,axiom, % 0.45/0.98 (! [X0_iProver_young_1,X0_iProver_seat_1] : % 0.45/0.98 ( in(X0_iProver_young_1,X0_iProver_seat_1) <=> % 0.45/0.98 ( % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1=skc21 & X0_iProver_seat_1=skc22 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1=skc16 & X0_iProver_seat_1=skc17 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_young_1=skc15 & X0_iProver_seat_1=skc18 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 | % 0.45/0.98 ( % 0.45/0.98 ( X0_iProver_seat_1=skc18 ) % 0.45/0.98 & % 0.45/0.98 ( X0_iProver_young_1!=skc16 ) % 0.45/0.98 ) % 0.45/0.98 % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ) % 0.45/0.98 ). % 0.45/0.98 % SZS output end Model for theBenchmark.p % 0.45/0.98 %------------------------------------------------------------------------------