%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ028-3 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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.36s 1.38s
% Output : Saturation 3.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u525,negated_conjecture,
~ not_familiar(n5,n6) ).
cnf(u528,negated_conjecture,
~ not_familiar(n6,n5) ).
cnf(u531,negated_conjecture,
~ not_familiar(n6,n6) ).
cnf(u535,negated_conjecture,
~ not_familiar(n4,n6) ).
cnf(u1193,negated_conjecture,
not_familiar(n6,n4) ).
cnf(u542,negated_conjecture,
~ not_familiar(n3,n6) ).
cnf(u1334,negated_conjecture,
not_familiar(n2,n6) ).
cnf(u552,negated_conjecture,
~ not_familiar(n6,n2) ).
cnf(u1370,negated_conjecture,
not_familiar(n1,n6) ).
cnf(u559,negated_conjecture,
~ not_familiar(n6,n1) ).
cnf(u564,negated_conjecture,
~ not_familiar(n5,n5) ).
cnf(u1238,negated_conjecture,
not_familiar(n5,n4) ).
cnf(u1244,negated_conjecture,
not_familiar(n5,n3) ).
cnf(u576,negated_conjecture,
~ not_familiar(n5,n2) ).
cnf(u580,negated_conjecture,
~ not_familiar(n5,n1) ).
cnf(u585,negated_conjecture,
~ not_familiar(n4,n5) ).
cnf(u589,negated_conjecture,
~ not_familiar(n4,n4) ).
cnf(u593,negated_conjecture,
~ not_familiar(n4,n3) ).
cnf(u597,negated_conjecture,
~ not_familiar(n4,n2) ).
cnf(u601,negated_conjecture,
~ not_familiar(n4,n1) ).
cnf(u1304,negated_conjecture,
not_familiar(n3,n5) ).
cnf(u1310,negated_conjecture,
not_familiar(n3,n4) ).
cnf(u614,negated_conjecture,
~ not_familiar(n3,n3) ).
cnf(u618,negated_conjecture,
~ not_familiar(n3,n2) ).
cnf(u622,negated_conjecture,
~ not_familiar(n3,n1) ).
cnf(u1340,negated_conjecture,
not_familiar(n2,n5) ).
cnf(u1346,negated_conjecture,
not_familiar(n2,n4) ).
cnf(u1352,negated_conjecture,
not_familiar(n2,n3) ).
cnf(u639,negated_conjecture,
~ not_familiar(n2,n2) ).
cnf(u1364,negated_conjecture,
not_familiar(n2,n1) ).
cnf(u1376,negated_conjecture,
not_familiar(n1,n5) ).
cnf(u1382,negated_conjecture,
not_familiar(n1,n4) ).
cnf(u1388,negated_conjecture,
not_familiar(n1,n3) ).
cnf(u1394,negated_conjecture,
not_familiar(n1,n2) ).
cnf(u664,negated_conjecture,
~ not_familiar(n1,n1) ).
cnf(u1227,negated_conjecture,
familiar(n5,n6) ).
cnf(u1185,negated_conjecture,
familiar(n6,n5) ).
cnf(u854,negated_conjecture,
~ familiar(n6,n6) ).
cnf(u1263,negated_conjecture,
familiar(n4,n6) ).
cnf(u861,negated_conjecture,
~ familiar(n6,n4) ).
cnf(u1299,negated_conjecture,
familiar(n3,n6) ).
cnf(u1203,negated_conjecture,
familiar(n6,n3) ).
cnf(u872,negated_conjecture,
~ familiar(n2,n6) ).
cnf(u1212,negated_conjecture,
familiar(n6,n2) ).
cnf(u879,negated_conjecture,
~ familiar(n1,n6) ).
cnf(u1221,negated_conjecture,
familiar(n6,n1) ).
cnf(u887,negated_conjecture,
~ familiar(n5,n5) ).
cnf(u891,negated_conjecture,
~ familiar(n5,n4) ).
cnf(u895,negated_conjecture,
~ familiar(n5,n3) ).
cnf(u1251,negated_conjecture,
familiar(n5,n2) ).
cnf(u1257,negated_conjecture,
familiar(n5,n1) ).
cnf(u1269,negated_conjecture,
familiar(n4,n5) ).
cnf(u912,negated_conjecture,
~ familiar(n4,n4) ).
cnf(u1281,negated_conjecture,
familiar(n4,n3) ).
cnf(u1287,negated_conjecture,
familiar(n4,n2) ).
cnf(u1293,negated_conjecture,
familiar(n4,n1) ).
cnf(u929,negated_conjecture,
~ familiar(n3,n5) ).
cnf(u933,negated_conjecture,
~ familiar(n3,n4) ).
cnf(u937,negated_conjecture,
~ familiar(n3,n3) ).
cnf(u1323,negated_conjecture,
familiar(n3,n2) ).
cnf(u1329,negated_conjecture,
familiar(n3,n1) ).
cnf(u950,negated_conjecture,
~ familiar(n2,n5) ).
cnf(u954,negated_conjecture,
~ familiar(n2,n4) ).
cnf(u958,negated_conjecture,
~ familiar(n2,n3) ).
cnf(u962,negated_conjecture,
~ familiar(n2,n2) ).
cnf(u966,negated_conjecture,
~ familiar(n2,n1) ).
cnf(u971,negated_conjecture,
~ familiar(n1,n5) ).
cnf(u975,negated_conjecture,
~ familiar(n1,n4) ).
cnf(u979,negated_conjecture,
~ familiar(n1,n3) ).
cnf(u983,negated_conjecture,
~ familiar(n1,n2) ).
cnf(u987,negated_conjecture,
~ familiar(n1,n1) ).
cnf(u1171,axiom,
~ not_equal(n6,n6) ).
cnf(u1231,axiom,
~ not_equal(n5,n5) ).
cnf(u1273,axiom,
~ not_equal(n4,n4) ).
cnf(u1315,axiom,
~ not_equal(n3,n3) ).
cnf(u1357,axiom,
~ not_equal(n2,n2) ).
cnf(u1399,axiom,
~ not_equal(n1,n1) ).
cnf(not_equal_1_4,axiom,
not_equal(n1,n4) ).
cnf(not_equal_3_4,axiom,
not_equal(n3,n4) ).
cnf(not_equal_6_3,axiom,
not_equal(n6,n3) ).
cnf(not_equal_2_1,axiom,
not_equal(n2,n1) ).
cnf(not_equal_6_5,axiom,
not_equal(n6,n5) ).
cnf(not_equal_5_1,axiom,
not_equal(n5,n1) ).
cnf(not_equal_4_1,axiom,
not_equal(n4,n1) ).
cnf(not_equal_4_3,axiom,
not_equal(n4,n3) ).
cnf(not_equal_5_6,axiom,
not_equal(n5,n6) ).
cnf(not_equal_3_6,axiom,
not_equal(n3,n6) ).
cnf(not_equal_3_5,axiom,
not_equal(n3,n5) ).
cnf(not_equal_5_4,axiom,
not_equal(n5,n4) ).
cnf(not_equal_6_1,axiom,
not_equal(n6,n1) ).
cnf(person_3,axiom,
person(n3) ).
cnf(not_equal_1_6,axiom,
not_equal(n1,n6) ).
cnf(not_equal_5_3,axiom,
not_equal(n5,n3) ).
cnf(person_6,axiom,
person(n6) ).
cnf(not_equal_6_4,axiom,
not_equal(n6,n4) ).
cnf(not_equal_1_3,axiom,
not_equal(n1,n3) ).
cnf(not_equal_3_2,axiom,
not_equal(n3,n2) ).
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(not_equal_4_6,axiom,
not_equal(n4,n6) ).
cnf(person_5,axiom,
person(n5) ).
cnf(not_equal_2_5,axiom,
not_equal(n2,n5) ).
cnf(not_equal_3_1,axiom,
not_equal(n3,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(person_2,axiom,
person(n2) ).
cnf(not_equal_6_2,axiom,
not_equal(n6,n2) ).
cnf(not_equal_1_5,axiom,
not_equal(n1,n5) ).
cnf(not_equal_5_2,axiom,
not_equal(n5,n2) ).
cnf(person_1,axiom,
person(n1) ).
cnf(not_equal_1_2,axiom,
not_equal(n1,n2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ028-3 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n002.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 22:33:22 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.36/1.38 % (3953928)Input is clausal, will run a generic CNF schedule.
% 3.36/1.38 % (3953934)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=797732551:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.36/1.38 % (3953935)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3800414573:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.36/1.38 % (3953940)dis-21_1_sil=8000:lcm=predicate:random_seed=1710668568: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.36/1.38 % (3953939)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=105087955:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.36/1.38 % (3953937)lrs+10_1_sil=8000:sp=occurrence:random_seed=3512872277:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.36/1.38 % (3953938)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3335720838:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.36/1.38 % (3953936)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=506269738:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.36/1.38 % (3953937)Refutation not found, incomplete strategy
% 3.36/1.38 % (3953937)------------------------------
% 3.36/1.38 % (3953937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.36/1.38 % (3953938)Refutation not found, incomplete strategy
% 3.36/1.38 % (3953938)------------------------------
% 3.36/1.38 % (3953938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.36/1.38 % (3953937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.36/1.38 % (3953938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.36/1.38 % (3953938)CaDiCaL version: 2.1.3
% 3.36/1.38 % (3953937)CaDiCaL version: 2.1.3
% 3.36/1.38 % (3953938)Termination reason: Refutation not found, incomplete strategy
% 3.36/1.38 % (3953938)Time elapsed: 0.002 s
% 3.36/1.38 % (3953937)Termination reason: Refutation not found, incomplete strategy
% 3.36/1.38 % (3953937)Time elapsed: 0.002 s
% 3.36/1.38 % (3953937)Peak memory usage: 87 MB
% 3.36/1.38 % (3953938)Peak memory usage: 87 MB
% 3.36/1.38 % (3953937)Instructions burned: 2 (million)
% 3.36/1.38 % (3953938)Instructions burned: 2 (million)
% 3.36/1.38 % (3953939)Refutation not found, incomplete strategy
% 3.36/1.38 % (3953939)------------------------------
% 3.36/1.38 % (3953939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.36/1.38 % (3953939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.36/1.38 % (3953939)CaDiCaL version: 2.1.3
% 3.36/1.38 % (3953939)Termination reason: Refutation not found, incomplete strategy
% 3.36/1.38 % (3953939)Time elapsed: 0.009 s
% 3.36/1.38 % (3953939)Peak memory usage: 89 MB
% 3.36/1.38 % (3953939)Instructions burned: 17 (million)
% 3.36/1.38 % (3953940)First to succeed.
% 3.36/1.38 % (3953940)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3953928"
% 3.36/1.38 [W927 22:33:23.028163479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 [W927 22:33:23.028187119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 [W927 22:33:23.028207088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 [W927 22:33:23.028213518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 [W927 22:33:23.028231245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 [W927 22:33:23.028239682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.36/1.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.36/1.38 % (3953938)------------------------------
% 3.36/1.38 % (3953938)------------------------------
% 3.36/1.38 % (3953937)------------------------------
% 3.36/1.38 % (3953937)------------------------------
% 3.36/1.38 % (3953939)------------------------------
% 3.36/1.38 % (3953939)------------------------------
% 3.36/1.38 % SZS status Satisfiable for theBenchmark
% 3.36/1.38 % SZS output start Saturation.
% See solution above
% 3.36/1.38 % SZS output start Definitions and Model Updates.
% 3.36/1.38 % SZS output end Definitions and Model Updates.
% 3.36/1.38 % (3953940)------------------------------
% 3.36/1.38 % (3953940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.36/1.38 % (3953940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.36/1.38 % (3953940)CaDiCaL version: 2.1.3
% 3.36/1.38 % (3953940)Termination reason: Satisfiable
% 3.36/1.38 % (3953940)Time elapsed: 0.010 s
% 3.36/1.38 % (3953940)Peak memory usage: 89 MB
% 3.36/1.38 % (3953940)Instructions burned: 17 (million)
% 3.36/1.38 % (3953940)------------------------------
% 3.36/1.38 % (3953940)------------------------------
% 3.36/1.38 % (3953928)Success in time 0.418 s
% 3.36/1.38 % Vampire exiting
%------------------------------------------------------------------------------