%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ028-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 : Tue Sep 29 12:31:16 PM UTC 2026
% Result : Satisfiable 3.53s 1.47s
% Output : Saturation 3.53s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u132,axiom,
~ familiar(n6,n5) ).
cnf(u137,axiom,
not_familiar(n6,n5) ).
cnf(u142,axiom,
familiar(n6,n4) ).
cnf(u145,axiom,
~ not_familiar(n6,n4) ).
cnf(u151,axiom,
familiar(n6,n3) ).
cnf(u160,axiom,
familiar(n6,n2) ).
cnf(u169,axiom,
familiar(n6,n1) ).
cnf(u177,axiom,
~ familiar(n5,n6) ).
cnf(u182,axiom,
not_familiar(n5,n6) ).
cnf(u187,axiom,
familiar(n5,n4) ).
cnf(u190,axiom,
~ not_familiar(n5,n4) ).
cnf(u196,axiom,
familiar(n5,n3) ).
cnf(u199,axiom,
~ not_familiar(n5,n3) ).
cnf(u204,axiom,
~ familiar(n5,n2) ).
cnf(u209,axiom,
not_familiar(n5,n2) ).
cnf(u213,axiom,
~ familiar(n5,n1) ).
cnf(u218,axiom,
not_familiar(n5,n1) ).
cnf(u222,axiom,
~ familiar(n4,n6) ).
cnf(u227,axiom,
not_familiar(n4,n6) ).
cnf(u231,axiom,
~ familiar(n4,n5) ).
cnf(u236,axiom,
not_familiar(n4,n5) ).
cnf(u240,axiom,
~ familiar(n4,n3) ).
cnf(u245,axiom,
not_familiar(n4,n3) ).
cnf(u249,axiom,
~ familiar(n4,n2) ).
cnf(u254,axiom,
not_familiar(n4,n2) ).
cnf(u258,axiom,
~ familiar(n4,n1) ).
cnf(u263,axiom,
not_familiar(n4,n1) ).
cnf(u267,axiom,
~ familiar(n3,n6) ).
cnf(u272,axiom,
not_familiar(n3,n6) ).
cnf(u277,axiom,
familiar(n3,n5) ).
cnf(u286,axiom,
familiar(n3,n4) ).
cnf(u294,axiom,
~ familiar(n3,n2) ).
cnf(u299,axiom,
not_familiar(n3,n2) ).
cnf(u303,axiom,
~ familiar(n3,n1) ).
cnf(u308,axiom,
not_familiar(n3,n1) ).
cnf(u313,axiom,
familiar(n2,n6) ).
cnf(u316,axiom,
~ not_familiar(n2,n6) ).
cnf(u322,axiom,
familiar(n2,n5) ).
cnf(u325,axiom,
~ not_familiar(n2,n5) ).
cnf(u331,axiom,
familiar(n2,n4) ).
cnf(u334,axiom,
~ not_familiar(n2,n4) ).
cnf(u340,axiom,
familiar(n2,n3) ).
cnf(u343,axiom,
~ not_familiar(n2,n3) ).
cnf(u348,axiom,
~ familiar(n2,n1) ).
cnf(u353,axiom,
not_familiar(n2,n1) ).
cnf(u358,axiom,
familiar(n1,n6) ).
cnf(u361,axiom,
~ not_familiar(n1,n6) ).
cnf(u367,axiom,
familiar(n1,n5) ).
cnf(u370,axiom,
~ not_familiar(n1,n5) ).
cnf(u376,axiom,
familiar(n1,n4) ).
cnf(u379,axiom,
~ not_familiar(n1,n4) ).
cnf(u385,axiom,
familiar(n1,n3) ).
cnf(u388,axiom,
~ not_familiar(n1,n3) ).
cnf(u393,axiom,
~ familiar(n1,n2) ).
cnf(u398,axiom,
not_familiar(n1,n2) ).
cnf(not_equal_1_4,axiom,
not_equal(n1,n4) ).
cnf(not_equal_3_4,axiom,
not_equal(n3,n4) ).
cnf(u586,negated_conjecture,
~ not_familiar(n1,n1) ).
cnf(familiar_or_not,axiom,
( ~ not_equal(X0,X1)
| not_familiar(X0,X1)
| ~ person(X0)
| ~ person(X1)
| familiar(X0,X1) ) ).
cnf(u469,negated_conjecture,
( ~ not_familiar(n6,X0)
| ~ not_familiar(X0,n4) ) ).
cnf(u479,negated_conjecture,
( ~ not_familiar(n2,X0)
| ~ not_familiar(X0,n4) ) ).
cnf(u550,negated_conjecture,
( ~ familiar(n3,X0)
| ~ familiar(X0,n2) ) ).
cnf(u544,negated_conjecture,
( ~ familiar(n5,X0)
| ~ familiar(X0,n2) ) ).
cnf(u418,negated_conjecture,
~ not_familiar(n6,n6) ).
cnf(u464,negated_conjecture,
( ~ not_familiar(n2,X0)
| ~ not_familiar(X0,n5) ) ).
cnf(not_equal_5_1,axiom,
not_equal(n5,n1) ).
cnf(u401,negated_conjecture,
( ~ familiar(n4,X0)
| ~ familiar(X0,n6) ) ).
cnf(not_equal_5_4,axiom,
not_equal(n5,n4) ).
cnf(not_equal_2_1,axiom,
not_equal(n2,n1) ).
cnf(not_equal_4_1,axiom,
not_equal(n4,n1) ).
cnf(u487,negated_conjecture,
( ~ not_familiar(n1,X0)
| ~ not_familiar(X0,n4) ) ).
cnf(not_equal_4_3,axiom,
not_equal(n4,n3) ).
cnf(not_equal_6_3,axiom,
not_equal(n6,n3) ).
cnf(u499,negated_conjecture,
( ~ not_familiar(n5,X0)
| ~ not_familiar(X0,n4) ) ).
cnf(not_equal_3_5,axiom,
not_equal(n3,n5) ).
cnf(u507,negated_conjecture,
( ~ not_familiar(n6,X0)
| ~ not_familiar(X0,n3) ) ).
cnf(u538,negated_conjecture,
~ familiar(n2,n2) ).
cnf(not_equal_6_1,axiom,
not_equal(n6,n1) ).
cnf(person_3,axiom,
person(n3) ).
cnf(not_equal_3_6,axiom,
not_equal(n3,n6) ).
cnf(not_equal_5_6,axiom,
not_equal(n5,n6) ).
cnf(u419,negated_conjecture,
( ~ not_familiar(n6,X0)
| ~ not_familiar(X0,n5) ) ).
cnf(u534,negated_conjecture,
( ~ not_familiar(n1,X0)
| ~ not_familiar(X0,n3) ) ).
cnf(u546,negated_conjecture,
( ~ familiar(n4,X0)
| ~ familiar(X0,n2) ) ).
cnf(u402,negated_conjecture,
( ~ familiar(n3,X0)
| ~ familiar(X0,n6) ) ).
cnf(u420,negated_conjecture,
( ~ familiar(n4,X0)
| ~ familiar(X0,n5) ) ).
cnf(u525,negated_conjecture,
( ~ not_familiar(n2,X0)
| ~ not_familiar(X0,n3) ) ).
cnf(not_equal_1_6,axiom,
not_equal(n1,n6) ).
cnf(not_equal_5_3,axiom,
not_equal(n5,n3) ).
cnf(three_not_familiar,negated_conjecture,
( ~ not_familiar(X2,X0)
| ~ not_familiar(X1,X2)
| ~ not_familiar(X0,X1) ) ).
cnf(u570,negated_conjecture,
( ~ familiar(n5,X0)
| ~ familiar(X0,n1) ) ).
cnf(person_6,axiom,
person(n6) ).
cnf(not_equal_1_3,axiom,
not_equal(n1,n3) ).
cnf(not_equal_3_2,axiom,
not_equal(n3,n2) ).
cnf(u536,negated_conjecture,
( ~ familiar(n6,X0)
| ~ familiar(X0,n2) ) ).
cnf(u576,negated_conjecture,
( ~ familiar(n3,X0)
| ~ familiar(X0,n1) ) ).
cnf(u564,negated_conjecture,
( ~ familiar(n6,X0)
| ~ familiar(X0,n1) ) ).
cnf(u535,negated_conjecture,
~ familiar(n6,n6) ).
cnf(person_4,axiom,
person(n4) ).
cnf(not_equal_2_4,axiom,
not_equal(n2,n4) ).
cnf(not_equal_2_6,axiom,
not_equal(n2,n6) ).
cnf(u509,negated_conjecture,
~ familiar(n5,n5) ).
cnf(not_equal_4_6,axiom,
not_equal(n4,n6) ).
cnf(person_5,axiom,
person(n5) ).
cnf(u515,negated_conjecture,
~ familiar(n3,n3) ).
cnf(not_equal_2_5,axiom,
not_equal(n2,n5) ).
cnf(not_equal_3_1,axiom,
not_equal(n3,n1) ).
cnf(u403,negated_conjecture,
( ~ familiar(n2,X0)
| ~ familiar(X0,n6) ) ).
cnf(u404,negated_conjecture,
( ~ familiar(n1,X0)
| ~ familiar(X0,n6) ) ).
cnf(u574,negated_conjecture,
( ~ familiar(n4,X0)
| ~ familiar(X0,n1) ) ).
cnf(u565,negated_conjecture,
~ familiar(n1,n1) ).
cnf(not_equal_2_3,axiom,
not_equal(n2,n3) ).
cnf(not_equal_4_2,axiom,
not_equal(n4,n2) ).
cnf(not_equal_4_5,axiom,
not_equal(n4,n5) ).
cnf(u579,negated_conjecture,
~ not_familiar(n2,n2) ).
cnf(not_equal_6_4,axiom,
not_equal(n6,n4) ).
cnf(person_2,axiom,
person(n2) ).
cnf(u439,negated_conjecture,
( ~ not_familiar(n3,X0)
| ~ not_familiar(X0,n4) ) ).
cnf(u467,negated_conjecture,
( ~ not_familiar(n1,X0)
| ~ not_familiar(X0,n5) ) ).
cnf(u422,negated_conjecture,
~ not_familiar(n5,n5) ).
cnf(u560,negated_conjecture,
( ~ not_familiar(n1,X0)
| ~ not_familiar(X0,n2) ) ).
cnf(not_equal_6_2,axiom,
not_equal(n6,n2) ).
cnf(not_equal_6_5,axiom,
not_equal(n6,n5) ).
cnf(not_equal_1_5,axiom,
not_equal(n1,n5) ).
cnf(not_equal_5_2,axiom,
not_equal(n5,n2) ).
cnf(three_familiar,negated_conjecture,
( ~ familiar(X2,X0)
| ~ familiar(X1,X2)
| ~ familiar(X0,X1) ) ).
cnf(person_1,axiom,
person(n1) ).
cnf(u583,negated_conjecture,
( ~ not_familiar(n2,X0)
| ~ not_familiar(X0,n1) ) ).
cnf(u514,negated_conjecture,
( ~ familiar(n4,X0)
| ~ familiar(X0,n3) ) ).
cnf(u498,negated_conjecture,
( ~ familiar(n3,X0)
| ~ familiar(X0,n5) ) ).
cnf(u511,negated_conjecture,
( ~ familiar(n5,X0)
| ~ familiar(X0,n3) ) ).
cnf(u400,negated_conjecture,
( ~ not_familiar(n5,X0)
| ~ not_familiar(X0,n6) ) ).
cnf(not_equal_1_2,axiom,
not_equal(n1,n2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ028-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 22:31:02 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.53/1.47 % (1370908)Input is clausal, will run a generic CNF schedule.
% 3.53/1.47 % (1370970)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3411798227:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.53/1.47 % (1370979)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2782330255:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.53/1.47 % (1370972)lrs+10_1_sil=8000:sp=occurrence:random_seed=1521855888:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.53/1.47 % (1370969)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1843140185:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.53/1.47 % (1370973)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3703360333:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.53/1.47 % (1370971)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1732344739:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.53/1.47 % (1370979)Refutation not found, incomplete strategy
% 3.53/1.47 % (1370979)------------------------------
% 3.53/1.47 % (1370979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1370979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1370979)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1370979)Termination reason: Refutation not found, incomplete strategy
% 3.53/1.47 % (1370979)Time elapsed: 0.004 s
% 3.53/1.47 % (1370979)Peak memory usage: 88 MB
% 3.53/1.47 % (1370979)Instructions burned: 9 (million)
% 3.53/1.47 % (1370972)First to succeed.
% 3.53/1.47 % (1370972)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1370908"
% 3.53/1.47 % (1370982)dis-21_1_sil=8000:lcm=predicate:random_seed=793914098:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.53/1.47 % (1370973)Instruction limit reached!
% 3.53/1.47 % (1370973)------------------------------
% 3.53/1.47 % (1370973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1370973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1370973)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1370973)Termination reason: Instruction limit
% 3.53/1.47 % (1370973)Termination phase: Saturation
% 3.53/1.47 % (1370973)Time elapsed: 0.043 s
% 3.53/1.47 % (1370973)Peak memory usage: 87 MB
% 3.53/1.47 % (1370973)Instructions burned: 115 (million)
% 3.53/1.47 % (1370982)Instruction limit reached!
% 3.53/1.47 % (1370982)------------------------------
% 3.53/1.47 % (1370982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1370982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1370982)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1370982)Termination reason: Instruction limit
% 3.53/1.47 % (1370982)Termination phase: Saturation
% 3.53/1.47 % (1370982)Time elapsed: 0.047 s
% 3.53/1.47 % (1370982)Peak memory usage: 87 MB
% 3.53/1.47 % (1370982)Instructions burned: 119 (million)
% 3.53/1.47 % (1370979)------------------------------
% 3.53/1.47 % (1370979)------------------------------
% 3.53/1.47 % (1370994)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=742219642:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.53/1.47 % (1370994)Refutation not found, incomplete strategy
% 3.53/1.47 % (1370994)------------------------------
% 3.53/1.47 % (1370994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1370994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1370994)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1370994)Termination reason: Refutation not found, incomplete strategy
% 3.53/1.47 % (1370994)Time elapsed: 0.001 s
% 3.53/1.47 % (1370994)Peak memory usage: 86 MB
% 3.53/1.47 % (1371013)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2214533195:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.53/1.47 % (1371013)Refutation not found, incomplete strategy
% 3.53/1.47 % (1371013)------------------------------
% 3.53/1.47 % (1371013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1371013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1371013)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1371013)Termination reason: Refutation not found, incomplete strategy
% 3.53/1.47 % (1371013)Time elapsed: 0.002 s
% 3.53/1.47 % (1371013)Peak memory usage: 87 MB
% 3.53/1.47 % (1371013)Instructions burned: 1 (million)
% 3.53/1.47 % SZS status Satisfiable for theBenchmark
% 3.53/1.47 % SZS output start Saturation.
% See solution above
% 3.53/1.47 % SZS output start Definitions and Model Updates.
% 3.53/1.47 % SZS output end Definitions and Model Updates.
% 3.53/1.47 % (1370972)------------------------------
% 3.53/1.47 % (1370972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.47 % (1370972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.47 % (1370972)CaDiCaL version: 2.1.3
% 3.53/1.47 % (1370972)Termination reason: Satisfiable
% 3.53/1.47 % (1370972)Time elapsed: 0.006 s
% 3.53/1.47 % (1370972)Peak memory usage: 88 MB
% 3.53/1.47 % (1370972)Instructions burned: 7 (million)
% 3.53/1.47 % (1370972)------------------------------
% 3.53/1.47 % (1370972)------------------------------
% 3.53/1.47 % (1370908)Success in time 0.422 s
% 3.53/1.47 % Vampire exiting
%------------------------------------------------------------------------------