%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT020-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 09:36:40 AM UTC 2026
% Result : Satisfiable 12.54s 2.49s
% Output : Saturation 12.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(category_theory_axiom6,axiom,
( ~ defined(X1,X2)
| ~ defined(X0,X1)
| ~ identity_map(X1)
| defined(X0,X2) ) ).
cnf(u65,axiom,
( defined(X0,codomain(X1))
| ~ defined(X0,X1) ) ).
cnf(u1648,axiom,
( ~ identity_map(X0)
| defined(codomain(X0),domain(X0)) ) ).
cnf(u1967,axiom,
( ~ defined(X2,domain(X0))
| ~ defined(X0,X1)
| defined(X2,codomain(X1)) ) ).
cnf(u1764,axiom,
( ~ product(X0,domain(X0),X1)
| product(X1,domain(X0),X0) ) ).
cnf(u291,axiom,
( ~ defined(X2,domain(X0))
| ~ defined(X0,X1)
| defined(X2,X1) ) ).
cnf(u302,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X0)
| product(X0,codomain(X1),codomain(X1)) ) ).
cnf(mapping_from_x_to_its_domain,axiom,
defined(X0,domain(X0)) ).
cnf(u101,axiom,
( ~ defined(X0,codomain(X1))
| defined(X0,X1) ) ).
cnf(u287,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X1)
| product(domain(X0),X1,domain(X0)) ) ).
cnf(u289,axiom,
( ~ defined(X0,X1)
| product(domain(X0),X1,compose(domain(X0),X1)) ) ).
cnf(u1681,axiom,
codomain(X0) = compose(codomain(X0),codomain(X0)) ).
cnf(u1901,axiom,
( ~ defined(domain(X1),X2)
| ~ defined(X0,domain(X1))
| defined(X0,X2) ) ).
cnf(u300,axiom,
( ~ defined(X2,X0)
| ~ defined(X0,X1)
| ~ identity_map(X0)
| defined(X2,codomain(X1)) ) ).
cnf(u30,axiom,
( ~ identity_map(X0)
| product(X0,domain(X0),domain(X0)) ) ).
cnf(u1262,axiom,
( ~ product(codomain(X2),X0,X3)
| ~ product(X0,X1,codomain(X2))
| product(X3,X1,codomain(X2)) ) ).
cnf(u2161,axiom,
( ~ defined(codomain(X0),X1)
| defined(domain(X2),codomain(X1))
| ~ defined(X2,X0) ) ).
cnf(u1035,axiom,
( ~ product(domain(X0),domain(X0),X1)
| domain(X0) = X1 ) ).
cnf(associative_property2,axiom,
( ~ product(X0,X1,X2)
| ~ defined(X2,X3)
| defined(X1,X3) ) ).
cnf(u145,axiom,
( ~ product(X0,codomain(X1),X2)
| ~ defined(X2,X1)
| defined(X0,X1) ) ).
cnf(u132,axiom,
( ~ product(codomain(X0),X0,X1)
| X0 = X1 ) ).
cnf(u2239,axiom,
( ~ defined(codomain(X1),X2)
| defined(domain(X0),X2)
| ~ defined(X0,codomain(X1)) ) ).
cnf(u2295,axiom,
( ~ defined(codomain(X1),X2)
| defined(X0,codomain(X2))
| ~ defined(X0,codomain(X1)) ) ).
cnf(u1650,axiom,
( ~ defined(X1,X0)
| defined(domain(X1),domain(X0))
| ~ identity_map(X0) ) ).
cnf(u1951,axiom,
( ~ defined(X0,X1)
| product(domain(X0),codomain(X1),compose(domain(X0),codomain(X1))) ) ).
cnf(u1902,axiom,
( ~ defined(codomain(X1),X2)
| ~ defined(X0,codomain(X1))
| defined(X0,X2) ) ).
cnf(u2163,axiom,
( ~ defined(domain(X0),X1)
| defined(X0,codomain(X1)) ) ).
cnf(u201,axiom,
( ~ product(X0,X1,codomain(X2))
| ~ product(X1,X2,X3)
| product(X0,X3,X2) ) ).
cnf(codomain_is_an_identity_map,axiom,
identity_map(codomain(X0)) ).
cnf(u96,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X1)
| defined(X0,domain(X1)) ) ).
cnf(u1261,axiom,
( ~ product(codomain(X0),codomain(X0),X1)
| codomain(X0) = X1 ) ).
cnf(u39,axiom,
defined(domain(X0),domain(X0)) ).
cnf(category_theory_axiom3,axiom,
( ~ product(X0,X1,X2)
| ~ defined(X3,X2)
| defined(X3,X0) ) ).
cnf(u471,axiom,
( ~ defined(X0,codomain(X1))
| defined(domain(X0),X1) ) ).
cnf(category_theory_axiom5,axiom,
( ~ product(X3,X2,X4)
| ~ product(X0,X1,X2)
| ~ product(X3,X0,X5)
| product(X5,X1,X4) ) ).
cnf(u1665,axiom,
domain(X0) = compose(domain(X0),domain(X0)) ).
cnf(composition_is_well_defined,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| X2 = X3 ) ).
cnf(u2357,axiom,
( ~ defined(X2,domain(X0))
| defined(domain(X2),codomain(X1))
| ~ defined(X0,X1) ) ).
cnf(u1944,axiom,
( ~ product(codomain(X0),codomain(X0),X1)
| product(codomain(X0),X1,codomain(X0)) ) ).
cnf(identity1,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X0)
| product(X0,X1,X1) ) ).
cnf(u1263,axiom,
( ~ product(X1,codomain(X2),X3)
| product(X0,X3,codomain(X2))
| ~ product(X0,X1,codomain(X2)) ) ).
cnf(u1120,axiom,
codomain(X0) = domain(codomain(X0)) ).
cnf(category_theory_axiom1,axiom,
( ~ product(X1,X3,X4)
| ~ product(X0,X1,X2)
| ~ defined(X2,X3)
| defined(X0,X4) ) ).
cnf(u49,axiom,
product(domain(X0),domain(X0),domain(X0)) ).
cnf(product_on_domain,axiom,
product(X0,domain(X0),X0) ).
cnf(u131,axiom,
( ~ product(X0,domain(X0),X1)
| X0 = X1 ) ).
cnf(u44,axiom,
( defined(domain(X0),X1)
| ~ defined(X0,X1) ) ).
cnf(u1037,axiom,
( ~ product(X1,domain(X2),X3)
| product(X0,X3,domain(X2))
| ~ product(X0,X1,domain(X2)) ) ).
cnf(category_theory_axiom2,axiom,
( ~ product(X2,X3,X4)
| ~ product(X0,X1,X2)
| ~ product(X1,X3,X5)
| product(X0,X5,X4) ) ).
cnf(product_on_codomain,axiom,
product(codomain(X0),X0,X0) ).
cnf(identity2,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X1)
| product(X0,X1,X0) ) ).
cnf(u543,axiom,
compose(codomain(X0),X0) = X0 ).
cnf(u304,axiom,
( ~ defined(X0,X1)
| product(X0,codomain(X1),X0) ) ).
cnf(u303,axiom,
( ~ defined(X0,X1)
| product(X0,codomain(X1),compose(X0,codomain(X1))) ) ).
cnf(u1938,axiom,
( defined(domain(X0),codomain(X1))
| ~ defined(X0,X1) ) ).
cnf(u234,axiom,
( ~ product(codomain(X2),X0,X3)
| ~ product(X0,X1,X2)
| product(X3,X1,X2) ) ).
cnf(u2448,axiom,
( ~ defined(codomain(X1),X2)
| defined(domain(X0),codomain(X2))
| ~ defined(X0,codomain(X1)) ) ).
cnf(mapping_from_codomain_of_x_to_x,axiom,
defined(codomain(X0),X0) ).
cnf(u169,axiom,
( ~ product(domain(X0),X1,X2)
| ~ defined(X0,X2)
| defined(X0,X1) ) ).
cnf(u2158,axiom,
( ~ defined(X2,X0)
| ~ identity_map(X0)
| defined(domain(X2),codomain(X1))
| ~ defined(X0,X1) ) ).
cnf(u2282,axiom,
( ~ defined(domain(X1),X2)
| defined(X0,codomain(X2))
| ~ defined(X0,domain(X1)) ) ).
cnf(u1943,axiom,
( ~ product(domain(X0),domain(X0),X1)
| product(domain(X0),X1,domain(X0)) ) ).
cnf(u2238,axiom,
( ~ defined(domain(X1),X2)
| defined(domain(X0),X2)
| ~ defined(X0,domain(X1)) ) ).
cnf(associative_property1,axiom,
( ~ product(X0,X1,X2)
| defined(X0,X1) ) ).
cnf(u1707,axiom,
( ~ product(codomain(X0),X0,X1)
| product(codomain(X0),X1,X0) ) ).
cnf(u2006,axiom,
( ~ product(domain(X0),domain(X0),X1)
| product(X1,domain(X0),domain(X0)) ) ).
cnf(u2162,axiom,
( ~ defined(codomain(X0),X1)
| defined(X2,codomain(X1))
| ~ defined(X2,X0) ) ).
cnf(u36,axiom,
( ~ identity_map(X0)
| product(codomain(X0),X0,codomain(X0)) ) ).
cnf(u233,axiom,
( ~ product(X0,X1,domain(X2))
| ~ product(X2,X0,X3)
| product(X3,X1,X2) ) ).
cnf(u290,axiom,
( ~ defined(X0,X1)
| product(domain(X0),X1,X1) ) ).
cnf(u61,axiom,
defined(codomain(X0),codomain(X0)) ).
cnf(u200,axiom,
( ~ product(X1,domain(X2),X3)
| ~ product(X0,X1,X2)
| product(X0,X3,X2) ) ).
cnf(domain_is_an_identity_map,axiom,
identity_map(domain(X0)) ).
cnf(u2007,axiom,
( ~ product(codomain(X0),codomain(X0),X1)
| product(X1,codomain(X0),codomain(X0)) ) ).
cnf(u1863,axiom,
( ~ defined(X0,X1)
| product(domain(X0),codomain(X1),domain(X0)) ) ).
cnf(u1406,axiom,
domain(X0) = codomain(domain(X0)) ).
cnf(u127,axiom,
compose(X0,domain(X0)) = X0 ).
cnf(closure_of_composition,axiom,
( ~ defined(X0,X1)
| product(X0,X1,compose(X0,X1)) ) ).
cnf(u1036,axiom,
( ~ product(domain(X2),X0,X3)
| ~ product(X0,X1,domain(X2))
| product(X3,X1,domain(X2)) ) ).
cnf(u2447,axiom,
( ~ defined(domain(X1),X2)
| defined(domain(X0),codomain(X2))
| ~ defined(X0,domain(X1)) ) ).
cnf(u1900,axiom,
( ~ defined(X2,domain(X0))
| defined(domain(X2),X1)
| ~ defined(X0,X1) ) ).
cnf(u2156,axiom,
( ~ defined(X0,X1)
| ~ identity_map(X0)
| defined(codomain(X0),codomain(X1)) ) ).
cnf(u159,axiom,
product(codomain(X0),codomain(X0),codomain(X0)) ).
cnf(category_theory_axiom4,axiom,
( ~ product(X3,X0,X4)
| ~ product(X0,X1,X2)
| ~ defined(X3,X2)
| defined(X4,X1) ) ).
cnf(u1550,axiom,
codomain(X0) = codomain(codomain(X0)) ).
cnf(u872,axiom,
domain(X0) = domain(domain(X0)) ).
cnf(u1843,axiom,
( ~ defined(X0,X1)
| product(domain(X0),codomain(X1),codomain(X1)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT020-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.18 % Computer : n007.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.18 % WCLimit : 300
% 0.11/0.18 % DateTime : Mon Sep 28 21:11:55 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.22 Running first-order theorem proving
% 0.11/0.22 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
% 7.59/1.90 % (2833541)Input is clausal, will run a generic CNF schedule.
% 7.59/1.90 % (2833551)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3262908395:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.59/1.90 % (2833549)lrs+10_1_sil=8000:sp=occurrence:random_seed=2484375079:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.59/1.90 % (2833550)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1276795918:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.59/1.90 % (2833546)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=2645319695:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.59/1.90 % (2833548)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3692689664:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.59/1.90 % (2833547)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3611948543:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.59/1.90 % (2833549)Refutation not found, incomplete strategy
% 7.59/1.90 % (2833549)------------------------------
% 7.59/1.90 % (2833549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.59/1.90 % (2833550)Refutation not found, incomplete strategy
% 7.59/1.90 % (2833550)------------------------------
% 7.59/1.90 % (2833550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.59/1.90 % (2833551)Instruction limit reached!
% 7.59/1.90 % (2833551)------------------------------
% 7.59/1.90 % (2833551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.59/1.90 % (2833549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.90 % (2833550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.90 % (2833551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.90 % (2833550)CaDiCaL version: 2.1.3
% 7.59/1.90 % (2833549)CaDiCaL version: 2.1.3
% 7.59/1.90 % (2833551)CaDiCaL version: 2.1.3
% 7.59/1.90 % (2833550)Termination reason: Refutation not found, incomplete strategy
% 7.59/1.90 % (2833550)Time elapsed: 0.024 s
% 7.59/1.90 % (2833549)Termination reason: Refutation not found, incomplete strategy
% 7.59/1.90 % (2833549)Time elapsed: 0.024 s
% 7.59/1.90 % (2833551)Termination reason: Instruction limit
% 7.59/1.90 % (2833551)Termination phase: Saturation
% 7.59/1.90 % (2833551)Time elapsed: 0.065 s
% 7.59/1.90 % (2833550)Peak memory usage: 86 MB
% 7.59/1.90 % (2833549)Peak memory usage: 86 MB
% 7.59/1.90 % (2833551)Peak memory usage: 88 MB
% 7.59/1.90 % (2833551)Instructions burned: 201 (million)
% 7.59/1.90 % (2833552)dis-21_1_sil=8000:lcm=predicate:random_seed=1475026074: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)
% 7.59/1.90 % (2833552)Refutation not found, incomplete strategy
% 7.59/1.90 % (2833552)------------------------------
% 7.59/1.90 % (2833552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.59/1.90 % (2833552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.90 % (2833552)CaDiCaL version: 2.1.3
% 7.59/1.90 % (2833552)Termination reason: Refutation not found, incomplete strategy
% 7.59/1.90 % (2833552)Time elapsed: 0.001 s
% 7.59/1.90 % (2833552)Peak memory usage: 86 MB
% 7.59/1.90 % (2833560)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=2831002478:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.59/1.90 % (2833560)Refutation not found, incomplete strategy
% 7.59/1.90 % (2833560)------------------------------
% 7.59/1.90 % (2833560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.59/1.90 % (2833560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.90 % (2833560)CaDiCaL version: 2.1.3
% 7.59/1.90 % (2833560)Termination reason: Refutation not found, incomplete strategy
% 7.59/1.90 % (2833560)Time elapsed: 0.0000 s
% 7.59/1.90 % (2833560)Peak memory usage: 86 MB
% 7.59/1.90 % (2833550)------------------------------
% 7.59/1.90 % (2833550)------------------------------
% 7.59/1.90 % (2833552)------------------------------
% 7.59/1.90 % (2833552)------------------------------
% 7.59/1.90 % (2833549)------------------------------
% 11.84/2.39 % (2833549)------------------------------
% 11.84/2.39 % (2833560)------------------------------
% 11.84/2.39 % (2833560)------------------------------
% 11.84/2.39 % (2833565)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2146764635:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.84/2.39 % (2833564)lrs+10_64_to=lpo:sil=8000:random_seed=3039476903:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.84/2.39 % (2833563)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=844201374:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 11.84/2.39 % (2833562)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1027072187:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 11.84/2.39 % (2833563)Refutation not found, incomplete strategy
% 11.84/2.39 % (2833563)------------------------------
% 11.84/2.39 % (2833563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833563)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833563)Termination reason: Refutation not found, incomplete strategy
% 11.84/2.39 % (2833563)Time elapsed: 0.0000 s
% 11.84/2.39 % (2833563)Peak memory usage: 86 MB
% 11.84/2.39 % (2833562)Refutation not found, incomplete strategy
% 11.84/2.39 % (2833562)------------------------------
% 11.84/2.39 % (2833562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833562)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833562)Termination reason: Refutation not found, incomplete strategy
% 11.84/2.39 % (2833562)Time elapsed: 0.0000 s
% 11.84/2.39 % (2833562)Peak memory usage: 86 MB
% 11.84/2.39 % (2833565)Instruction limit reached!
% 11.84/2.39 % (2833565)------------------------------
% 11.84/2.39 % (2833565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833565)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833565)Termination reason: Instruction limit
% 11.84/2.39 % (2833565)Termination phase: Saturation
% 11.84/2.39 % (2833565)Time elapsed: 0.069 s
% 11.84/2.39 % (2833565)Peak memory usage: 88 MB
% 11.84/2.39 % (2833565)Instructions burned: 195 (million)
% 11.84/2.39 % (2833564)Instruction limit reached!
% 11.84/2.39 % (2833564)------------------------------
% 11.84/2.39 % (2833564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833564)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833564)Termination reason: Instruction limit
% 11.84/2.39 % (2833564)Termination phase: Saturation
% 11.84/2.39 % (2833564)Time elapsed: 0.074 s
% 11.84/2.39 % (2833564)Peak memory usage: 88 MB
% 11.84/2.39 % (2833564)Instructions burned: 127 (million)
% 11.84/2.39 % (2833570)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1565393643:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 11.84/2.39 % (2833570)Instruction limit reached!
% 11.84/2.39 % (2833570)------------------------------
% 11.84/2.39 % (2833570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833570)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833570)Termination reason: Instruction limit
% 11.84/2.39 % (2833570)Termination phase: Saturation
% 11.84/2.39 % (2833570)Time elapsed: 0.054 s
% 11.84/2.39 % (2833570)Peak memory usage: 88 MB
% 11.84/2.39 % (2833570)Instructions burned: 164 (million)
% 11.84/2.39 % (2833563)------------------------------
% 11.84/2.39 % (2833563)------------------------------
% 11.84/2.39 % (2833562)------------------------------
% 11.84/2.39 % (2833562)------------------------------
% 11.84/2.39 % (2833571)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3735638030:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 11.84/2.39 % (2833573)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2810219911:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 11.84/2.39 % (2833573)Refutation not found, incomplete strategy
% 11.84/2.39 % (2833573)------------------------------
% 11.84/2.39 % (2833573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833573)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833573)Termination reason: Refutation not found, incomplete strategy
% 11.84/2.39 % (2833573)Time elapsed: 0.0000 s
% 11.84/2.39 % (2833573)Peak memory usage: 86 MB
% 11.84/2.39 % (2833575)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1539628843:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 11.84/2.39 % (2833574)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1702349219:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 11.84/2.39 % (2833575)Refutation not found, incomplete strategy
% 11.84/2.39 % (2833575)------------------------------
% 11.84/2.39 % (2833575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833575)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833575)Termination reason: Refutation not found, incomplete strategy
% 11.84/2.39 % (2833575)Time elapsed: 0.001 s
% 11.84/2.39 % (2833575)Peak memory usage: 86 MB
% 11.84/2.39 % (2833574)Refutation not found, incomplete strategy
% 11.84/2.39 % (2833574)------------------------------
% 11.84/2.39 % (2833574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.39 % (2833574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.39 % (2833574)CaDiCaL version: 2.1.3
% 11.84/2.39 % (2833574)Termination reason: Refutation not found, incomplete strategy
% 11.84/2.39 % (2833574)Time elapsed: 0.001 s
% 11.84/2.39 % (2833574)Peak memory usage: 87 MB
% 11.84/2.39 % (2833573)------------------------------
% 11.84/2.39 % (2833573)------------------------------
% 11.84/2.39 % (2833580)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2752810600:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 11.84/2.39 [W928 21:11:57.884206511 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884239511 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884277128 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884289861 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884316075 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884327941 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.39 [W928 21:11:57.884354581 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.
% 11.84/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 [W928 21:11:57.884366405 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.
% 12.54/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 [W928 21:11:57.884397941 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.
% 12.54/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 [W928 21:11:57.884465995 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.
% 12.54/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 [W928 21:11:57.884500958 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.
% 12.54/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 [W928 21:11:57.884512295 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.
% 12.54/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.54/2.49 % (2833574)------------------------------
% 12.54/2.49 % (2833574)------------------------------
% 12.54/2.49 % (2833575)------------------------------
% 12.54/2.49 % (2833575)------------------------------
% 12.54/2.49 % (2833571)Refutation not found, incomplete strategy
% 12.54/2.49 % (2833571)------------------------------
% 12.54/2.49 % (2833571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.49 % (2833571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.49 % (2833571)CaDiCaL version: 2.1.3
% 12.54/2.49 % (2833571)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.49 % (2833571)Time elapsed: 0.558 s
% 12.54/2.49 % (2833571)Peak memory usage: 125 MB
% 12.54/2.49 % (2833571)Instructions burned: 825 (million)
% 12.54/2.49 % (2833583)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2683562840:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 12.54/2.49 % (2833582)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1093595415:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 12.54/2.49 % (2833582)Refutation not found, incomplete strategy
% 12.54/2.49 % (2833582)------------------------------
% 12.54/2.49 % (2833582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.49 % (2833582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.49 % (2833582)CaDiCaL version: 2.1.3
% 12.54/2.49 % (2833582)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.49 % (2833582)Time elapsed: 0.001 s
% 12.54/2.49 % (2833582)Peak memory usage: 86 MB
% 12.54/2.49 % (2833583)First to succeed.
% 12.54/2.49 % (2833583)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2833541"
% 12.54/2.49 % (2833547)Refutation not found, incomplete strategy
% 12.54/2.49 % (2833547)------------------------------
% 12.54/2.49 % (2833547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.49 % (2833547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.49 % (2833547)CaDiCaL version: 2.1.3
% 12.54/2.49 % (2833547)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.49 % (2833547)Time elapsed: 1.308 s
% 12.54/2.49 % (2833547)Peak memory usage: 128 MB
% 12.54/2.49 % (2833547)Instructions burned: 2261 (million)
% 12.54/2.49 % (2833571)------------------------------
% 12.54/2.49 % (2833571)------------------------------
% 12.54/2.49 % (2833582)------------------------------
% 12.54/2.49 % (2833582)------------------------------
% 12.54/2.49 % SZS status Satisfiable for theBenchmark
% 12.54/2.49 % SZS output start Saturation.
% See solution above
% 12.54/2.49 % SZS output start Definitions and Model Updates.
% 12.54/2.49 % SZS output end Definitions and Model Updates.
% 12.54/2.49 % (2833583)------------------------------
% 12.54/2.49 % (2833583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.49 % (2833583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.49 % (2833583)CaDiCaL version: 2.1.3
% 12.54/2.49 % (2833583)Termination reason: Satisfiable
% 12.54/2.49 % (2833583)Time elapsed: 0.052 s
% 12.54/2.49 % (2833583)Peak memory usage: 88 MB
% 12.54/2.49 % (2833583)Instructions burned: 81 (million)
% 12.54/2.49 % (2833583)------------------------------
% 12.54/2.49 % (2833583)------------------------------
% 12.54/2.49 % (2833541)Success in time 1.722 s
% 12.54/2.49 % Vampire exiting
%------------------------------------------------------------------------------