%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL352-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 11:52:04 AM UTC 2026
% Result : Timeout 294.25s 43.70s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL352-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.46 % Computer : n015.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.47 % CPULimit : 300
% 0.19/0.47 % WCLimit : 300
% 0.19/0.47 % DateTime : Sun Sep 27 15:39:31 UTC 2026
% 0.19/0.47 % CPUTime :
% 0.19/0.47 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 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
% 18.85/3.98 % (1799974)Input is clausal, will run a generic CNF schedule.
% 18.85/3.98 % (1799984)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3886606079:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.85/3.98 % (1799984)Instruction limit reached!
% 18.85/3.98 % (1799984)------------------------------
% 18.85/3.98 % (1799984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.85/3.98 % (1799984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.85/3.98 % (1799984)CaDiCaL version: 2.1.3
% 18.85/3.98 % (1799984)Termination reason: Instruction limit
% 18.85/3.98 % (1799984)Termination phase: Saturation
% 18.85/3.98 % (1799984)Time elapsed: 0.056 s
% 18.85/3.98 % (1799984)Peak memory usage: 89 MB
% 18.85/3.98 % (1799984)Instructions burned: 116 (million)
% 18.85/3.98 % (1799980)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=2863765632:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.85/3.98 % (1799981)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=931458842:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.85/3.98 % (1799982)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3660177448:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.85/3.98 % (1799986)dis-21_1_sil=8000:lcm=predicate:random_seed=4066306727: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)
% 18.85/3.98 % (1799985)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1915520259:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.85/3.98 % (1799983)lrs+10_1_sil=8000:sp=occurrence:random_seed=1002145004:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.85/3.98 % (1799986)Instruction limit reached!
% 18.85/3.98 % (1799986)------------------------------
% 18.85/3.98 % (1799986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.85/3.98 % (1799986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.85/3.98 % (1799986)CaDiCaL version: 2.1.3
% 18.85/3.98 % (1799986)Termination reason: Instruction limit
% 18.85/3.98 % (1799986)Termination phase: Saturation
% 18.85/3.98 % (1799986)Time elapsed: 0.087 s
% 18.85/3.98 % (1799986)Peak memory usage: 87 MB
% 18.85/3.98 % (1799986)Instructions burned: 118 (million)
% 18.85/3.98 % (1799983)Instruction limit reached!
% 18.85/3.98 % (1799983)------------------------------
% 18.85/3.98 % (1799983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.85/3.98 % (1799983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.85/3.98 % (1799983)CaDiCaL version: 2.1.3
% 18.85/3.98 % (1799983)Termination reason: Instruction limit
% 18.85/3.98 % (1799983)Termination phase: Saturation
% 18.85/3.98 % (1799983)Time elapsed: 0.107 s
% 18.85/3.98 % (1799983)Peak memory usage: 89 MB
% 18.85/3.98 % (1799983)Instructions burned: 107 (million)
% 18.85/3.98 % (1799985)Instruction limit reached!
% 18.85/3.98 % (1799985)------------------------------
% 18.85/3.98 % (1799985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.85/3.98 % (1799985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.85/3.98 % (1799985)CaDiCaL version: 2.1.3
% 18.85/3.98 % (1799985)Termination reason: Instruction limit
% 18.85/3.98 % (1799985)Termination phase: Saturation
% 18.85/3.98 % (1799985)Time elapsed: 0.178 s
% 18.85/3.98 % (1799985)Peak memory usage: 89 MB
% 18.85/3.98 % (1799985)Instructions burned: 180 (million)
% 18.85/3.98 % (1799991)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=2872897011:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.85/3.98 % (1799991)Refutation not found, incomplete strategy
% 18.85/3.98 % (1799991)------------------------------
% 18.85/3.98 % (1799991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.85/3.98 % (1799991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.85/3.98 % (1799991)CaDiCaL version: 2.1.3
% 18.85/3.98 % (1799991)Termination reason: Refutation not found, incomplete strategy
% 18.85/3.98 % (1799991)Time elapsed: 0.001 s
% 18.85/3.98 % (1799991)Peak memory usage: 88 MB
% 18.85/3.98 % (1799995)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=720606357:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 34.55/6.10 % (1799995)Refutation not found, incomplete strategy
% 34.55/6.10 % (1799995)------------------------------
% 34.55/6.10 % (1799995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1799995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1799995)CaDiCaL version: 2.1.3
% 34.55/6.10 % (1799995)Termination reason: Refutation not found, incomplete strategy
% 34.55/6.10 % (1799995)Time elapsed: 0.002 s
% 34.55/6.10 % (1799995)Peak memory usage: 87 MB
% 34.55/6.10 % (1799995)Instructions burned: 1 (million)
% 34.55/6.10 % (1799996)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4015623573:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 34.55/6.10 % (1799996)Refutation not found, incomplete strategy
% 34.55/6.10 % (1799996)------------------------------
% 34.55/6.10 % (1799996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1799996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1799996)CaDiCaL version: 2.1.3
% 34.55/6.10 % (1799996)Termination reason: Refutation not found, incomplete strategy
% 34.55/6.10 % (1799996)Time elapsed: 0.002 s
% 34.55/6.10 % (1799996)Peak memory usage: 87 MB
% 34.55/6.10 % (1799991)------------------------------
% 34.55/6.10 % (1799991)------------------------------
% 34.55/6.10 % (1799997)lrs+10_64_to=lpo:sil=8000:random_seed=3493387973:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 34.55/6.10 % (1799997)Instruction limit reached!
% 34.55/6.10 % (1799997)------------------------------
% 34.55/6.10 % (1799997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1799997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1799997)CaDiCaL version: 2.1.3
% 34.55/6.10 % (1799997)Termination reason: Instruction limit
% 34.55/6.10 % (1799997)Termination phase: Saturation
% 34.55/6.10 % (1799997)Time elapsed: 0.119 s
% 34.55/6.10 % (1799997)Peak memory usage: 89 MB
% 34.55/6.10 % (1799997)Instructions burned: 126 (million)
% 34.55/6.10 % (1800002)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1877355974:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 34.55/6.10 % (1799995)------------------------------
% 34.55/6.10 % (1799995)------------------------------
% 34.55/6.10 % (1799996)------------------------------
% 34.55/6.10 % (1799996)------------------------------
% 34.55/6.10 % (1800002)Instruction limit reached!
% 34.55/6.10 % (1800002)------------------------------
% 34.55/6.10 % (1800002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1800002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1800002)CaDiCaL version: 2.1.3
% 34.55/6.10 % (1800002)Termination reason: Instruction limit
% 34.55/6.10 % (1800002)Termination phase: Saturation
% 34.55/6.10 % (1800002)Time elapsed: 0.098 s
% 34.55/6.10 % (1800002)Peak memory usage: 90 MB
% 34.55/6.10 % (1800002)Instructions burned: 195 (million)
% 34.55/6.10 % (1800003)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1818855738:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 34.55/6.10 % (1800005)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2296268312:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 34.55/6.10 % (1800007)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1470632419:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 34.55/6.10 % (1800007)Refutation not found, incomplete strategy
% 34.55/6.10 % (1800007)------------------------------
% 34.55/6.10 % (1800007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1800007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1800007)CaDiCaL version: 2.1.3
% 34.55/6.10 % (1800007)Termination reason: Refutation not found, incomplete strategy
% 34.55/6.10 % (1800007)Time elapsed: 0.001 s
% 34.55/6.10 % (1800007)Peak memory usage: 87 MB
% 34.55/6.10 % (1800003)Instruction limit reached!
% 34.55/6.10 % (1800003)------------------------------
% 34.55/6.10 % (1800003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.55/6.10 % (1800003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.55/6.10 % (1800003)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800003)Termination reason: Instruction limit
% 54.25/8.93 % (1800003)Termination phase: Saturation
% 54.25/8.93 % (1800003)Time elapsed: 0.158 s
% 54.25/8.93 % (1800003)Peak memory usage: 91 MB
% 54.25/8.93 % (1800003)Instructions burned: 157 (million)
% 54.25/8.93 % (1800006)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=1171763001:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 54.25/8.93 % (1800006)Instruction limit reached!
% 54.25/8.93 % (1800006)------------------------------
% 54.25/8.93 % (1800006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.93 % (1800006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.93 % (1800006)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800006)Termination reason: Instruction limit
% 54.25/8.93 % (1800006)Termination phase: Saturation
% 54.25/8.93 % (1800006)Time elapsed: 0.092 s
% 54.25/8.93 % (1800006)Peak memory usage: 88 MB
% 54.25/8.93 % (1800006)Instructions burned: 107 (million)
% 54.25/8.93 % (1800007)------------------------------
% 54.25/8.93 % (1800007)------------------------------
% 54.25/8.93 % (1800012)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3748618348:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 54.25/8.93 % (1800013)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3243246092:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 54.25/8.93 % (1800014)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3296779211:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 54.25/8.93 % (1800014)Instruction limit reached!
% 54.25/8.93 % (1800014)------------------------------
% 54.25/8.93 % (1800014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.93 % (1800014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.93 % (1800014)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800014)Termination reason: Instruction limit
% 54.25/8.93 % (1800014)Termination phase: Saturation
% 54.25/8.93 % (1800014)Time elapsed: 0.066 s
% 54.25/8.93 % (1800014)Peak memory usage: 89 MB
% 54.25/8.93 % (1800014)Instructions burned: 136 (million)
% 54.25/8.93 % (1800012)Instruction limit reached!
% 54.25/8.93 % (1800012)------------------------------
% 54.25/8.93 % (1800012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.93 % (1800012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.93 % (1800012)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800012)Termination reason: Instruction limit
% 54.25/8.93 % (1800012)Termination phase: Saturation
% 54.25/8.93 % (1800012)Time elapsed: 0.303 s
% 54.25/8.93 % (1800012)Peak memory usage: 90 MB
% 54.25/8.93 % (1800012)Instructions burned: 244 (million)
% 54.25/8.93 % (1800018)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1574652704:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 54.25/8.93 % (1800019)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=229463334:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 54.25/8.93 % (1800018)Instruction limit reached!
% 54.25/8.93 % (1800018)------------------------------
% 54.25/8.93 % (1800018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.93 % (1800018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.93 % (1800018)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800018)Termination reason: Instruction limit
% 54.25/8.93 % (1800018)Termination phase: Saturation
% 54.25/8.93 % (1800018)Time elapsed: 0.239 s
% 54.25/8.93 % (1800018)Peak memory usage: 95 MB
% 54.25/8.93 % (1800018)Instructions burned: 501 (million)
% 54.25/8.93 % (1800019)Instruction limit reached!
% 54.25/8.93 % (1800019)------------------------------
% 54.25/8.93 % (1800019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.93 % (1800019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.93 % (1800019)CaDiCaL version: 2.1.3
% 54.25/8.93 % (1800019)Termination reason: Instruction limit
% 54.25/8.93 % (1800019)Termination phase: Saturation
% 54.25/8.93 % (1800019)Time elapsed: 0.212 s
% 54.25/8.93 % (1800019)Peak memory usage: 93 MB
% 54.25/8.93 % (1800019)Instructions burned: 191 (million)
% 54.25/8.93 % (1800022)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1651840117:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 87.14/13.53 % (1800023)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2875202101:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 87.14/13.53 % (1800023)Instruction limit reached!
% 87.14/13.53 % (1800023)------------------------------
% 87.14/13.53 % (1800023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800023)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800023)Termination reason: Instruction limit
% 87.14/13.53 % (1800023)Termination phase: Saturation
% 87.14/13.53 % (1800023)Time elapsed: 0.139 s
% 87.14/13.53 % (1800023)Peak memory usage: 88 MB
% 87.14/13.53 % (1800023)Instructions burned: 156 (million)
% 87.14/13.53 % (1800022)Instruction limit reached!
% 87.14/13.53 % (1800022)------------------------------
% 87.14/13.53 % (1800022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800022)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800022)Termination reason: Instruction limit
% 87.14/13.53 % (1800022)Termination phase: Saturation
% 87.14/13.53 % (1800022)Time elapsed: 0.262 s
% 87.14/13.53 % (1800022)Peak memory usage: 92 MB
% 87.14/13.53 % (1800022)Instructions burned: 264 (million)
% 87.14/13.53 % (1800026)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1745690439:i=3256:kws=precedence:bd=preordered:av=off_2970 on theBenchmark for (2970ds/3256Mi)
% 87.14/13.53 % (1800027)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=386059802:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 87.14/13.53 % (1800027)Instruction limit reached!
% 87.14/13.53 % (1800027)------------------------------
% 87.14/13.53 % (1800027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800027)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800027)Termination reason: Instruction limit
% 87.14/13.53 % (1800027)Termination phase: Saturation
% 87.14/13.53 % (1800027)Time elapsed: 0.510 s
% 87.14/13.53 % (1800027)Peak memory usage: 91 MB
% 87.14/13.53 % (1800027)Instructions burned: 537 (million)
% 87.14/13.53 % (1800030)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2456552464:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 87.14/13.53 % (1800030)Instruction limit reached!
% 87.14/13.53 % (1800030)------------------------------
% 87.14/13.53 % (1800030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800030)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800030)Termination reason: Instruction limit
% 87.14/13.53 % (1800030)Termination phase: Saturation
% 87.14/13.53 % (1800030)Time elapsed: 0.160 s
% 87.14/13.53 % (1800030)Peak memory usage: 89 MB
% 87.14/13.53 % (1800030)Instructions burned: 181 (million)
% 87.14/13.53 % (1800032)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3626239584:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 87.14/13.53 % (1800005)Instruction limit reached!
% 87.14/13.53 % (1800005)------------------------------
% 87.14/13.53 % (1800005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800005)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800005)Termination reason: Instruction limit
% 87.14/13.53 % (1800005)Termination phase: Saturation
% 87.14/13.53 % (1800005)Time elapsed: 3.290 s
% 87.14/13.53 % (1800005)Peak memory usage: 148 MB
% 87.14/13.53 % (1800005)Instructions burned: 3394 (million)
% 87.14/13.53 % (1800013)Instruction limit reached!
% 87.14/13.53 % (1800013)------------------------------
% 87.14/13.53 % (1800013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.14/13.53 % (1800013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.14/13.53 % (1800013)CaDiCaL version: 2.1.3
% 87.14/13.53 % (1800013)Termination reason: Instruction limit
% 87.14/13.53 % (1800013)Termination phase: Saturation
% 87.14/13.53 % (1800013)Time elapsed: 3.101 s
% 117.45/17.89 % (1800013)Peak memory usage: 167 MB
% 117.45/17.89 % (1800013)Instructions burned: 5209 (million)
% 117.45/17.89 % (1800034)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4046937476:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 117.45/17.89 % (1800035)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1204636420:s2pl=no:i=8478:s2at=4:nm=6_2951 on theBenchmark for (2951ds/8478Mi)
% 117.45/17.89 % (1800034)Instruction limit reached!
% 117.45/17.89 % (1800034)------------------------------
% 117.45/17.89 % (1800034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.45/17.89 % (1800034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.45/17.89 % (1800034)CaDiCaL version: 2.1.3
% 117.45/17.89 % (1800034)Termination reason: Instruction limit
% 117.45/17.89 % (1800034)Termination phase: Saturation
% 117.45/17.89 % (1800034)Time elapsed: 0.392 s
% 117.45/17.89 % (1800034)Peak memory usage: 93 MB
% 117.45/17.89 % (1800034)Instructions burned: 412 (million)
% 117.45/17.89 % (1800038)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1651487212:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2946 on theBenchmark for (2946ds/303Mi)
% 117.45/17.89 % (1800038)Refutation not found, incomplete strategy
% 117.45/17.89 % (1800038)------------------------------
% 117.45/17.89 % (1800038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.45/17.89 % (1800038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.45/17.89 % (1800038)CaDiCaL version: 2.1.3
% 117.45/17.89 % (1800038)Termination reason: Refutation not found, incomplete strategy
% 117.45/17.89 % (1800038)Time elapsed: 0.002 s
% 117.45/17.89 % (1800038)Peak memory usage: 88 MB
% 117.45/17.89 % (1800038)------------------------------
% 117.45/17.89 % (1800038)------------------------------
% 117.45/17.89 % (1800040)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2705463437:st=4:i=720:sd=3:fsr=off:ss=axioms_2939 on theBenchmark for (2939ds/720Mi)
% 117.45/17.89 % (1800040)Refutation not found, incomplete strategy
% 117.45/17.89 % (1800040)------------------------------
% 117.45/17.89 % (1800040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.45/17.89 % (1800040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.45/17.89 % (1800040)CaDiCaL version: 2.1.3
% 117.45/17.89 % (1800040)Termination reason: Refutation not found, incomplete strategy
% 117.45/17.89 % (1800040)Time elapsed: 0.002 s
% 117.45/17.89 % (1800040)Peak memory usage: 88 MB
% 117.45/17.89 % (1800026)Instruction limit reached!
% 117.45/17.89 % (1800026)------------------------------
% 117.45/17.89 % (1800026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.45/17.89 % (1800026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.45/17.89 % (1800026)CaDiCaL version: 2.1.3
% 117.45/17.89 % (1800026)Termination reason: Instruction limit
% 117.45/17.89 % (1800026)Termination phase: Saturation
% 117.45/17.89 % (1800026)Time elapsed: 3.192 s
% 117.45/17.89 % (1800026)Peak memory usage: 150 MB
% 117.45/17.89 % (1800026)Instructions burned: 3257 (million)
% 117.45/17.89 % (1800040)------------------------------
% 117.45/17.89 % (1800040)------------------------------
% 117.45/17.89 % (1800042)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3720799677:i=598:bs=on:bd=preordered:av=off:ss=axioms_2935 on theBenchmark for (2935ds/598Mi)
% 117.45/17.89 % (1800043)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=529176257:i=2989:sd=3:ss=axioms:sgt=60_2933 on theBenchmark for (2933ds/2989Mi)
% 117.45/17.89 % (1800042)Instruction limit reached!
% 117.45/17.89 % (1800042)------------------------------
% 117.45/17.89 % (1800042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.45/17.89 % (1800042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.45/17.89 % (1800042)CaDiCaL version: 2.1.3
% 117.45/17.89 % (1800042)Termination reason: Instruction limit
% 117.45/17.89 % (1800042)Termination phase: Saturation
% 117.45/17.89 % (1800042)Time elapsed: 0.569 s
% 117.45/17.89 % (1800042)Peak memory usage: 96 MB
% 117.45/17.89 % (1800042)Instructions burned: 598 (million)
% 117.45/17.89 % (1800046)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1110222514:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 157.20/23.44 % (1800046)Instruction limit reached!
% 157.20/23.44 % (1800046)------------------------------
% 157.20/23.44 % (1800046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.20/23.44 % (1800046)CaDiCaL version: 2.1.3
% 157.20/23.44 % (1800046)Termination reason: Instruction limit
% 157.20/23.44 % (1800046)Termination phase: Saturation
% 157.20/23.44 % (1800046)Time elapsed: 2.076 s
% 157.20/23.44 % (1800046)Peak memory usage: 137 MB
% 157.20/23.44 % (1800046)Instructions burned: 1998 (million)
% 157.20/23.44 % (1800035)Instruction limit reached!
% 157.20/23.44 % (1800035)------------------------------
% 157.20/23.44 % (1800035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.20/23.44 % (1800035)CaDiCaL version: 2.1.3
% 157.20/23.44 % (1800035)Termination reason: Instruction limit
% 157.20/23.44 % (1800035)Termination phase: Saturation
% 157.20/23.44 % (1800035)Time elapsed: 4.684 s
% 157.20/23.44 % (1800035)Peak memory usage: 201 MB
% 157.20/23.44 % (1800035)Instructions burned: 8479 (million)
% 157.20/23.44 % (1800043)Instruction limit reached!
% 157.20/23.44 % (1800043)------------------------------
% 157.20/23.44 % (1800043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.20/23.44 % (1800043)CaDiCaL version: 2.1.3
% 157.20/23.44 % (1800043)Termination reason: Instruction limit
% 157.20/23.44 % (1800043)Termination phase: Saturation
% 157.20/23.44 % (1800043)Time elapsed: 2.933 s
% 157.20/23.44 % (1800043)Peak memory usage: 144 MB
% 157.20/23.44 % (1800043)Instructions burned: 2989 (million)
% 157.20/23.44 % (1800048)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2507239339:i=2088:bd=preordered:av=off_2902 on theBenchmark for (2902ds/2088Mi)
% 157.20/23.44 % (1800049)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=729514976:i=1098:nicw=on_2901 on theBenchmark for (2901ds/1098Mi)
% 157.20/23.44 % (1800050)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=280598999:i=433:bd=preordered_2900 on theBenchmark for (2900ds/433Mi)
% 157.20/23.44 % (1800049)Instruction limit reached!
% 157.20/23.44 % (1800049)------------------------------
% 157.20/23.44 % (1800049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.20/23.44 % (1800049)CaDiCaL version: 2.1.3
% 157.20/23.44 % (1800049)Termination reason: Instruction limit
% 157.20/23.44 % (1800049)Termination phase: Saturation
% 157.20/23.44 % (1800049)Time elapsed: 0.457 s
% 157.20/23.44 % (1800049)Peak memory usage: 103 MB
% 157.20/23.44 % (1800049)Instructions burned: 1100 (million)
% 157.20/23.44 % (1800050)Instruction limit reached!
% 157.20/23.44 % (1800050)------------------------------
% 157.20/23.44 % (1800050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.20/23.44 % (1800050)CaDiCaL version: 2.1.3
% 157.20/23.44 % (1800050)Termination reason: Instruction limit
% 157.20/23.44 % (1800050)Termination phase: Saturation
% 157.20/23.44 % (1800050)Time elapsed: 0.384 s
% 157.20/23.44 % (1800050)Peak memory usage: 93 MB
% 157.20/23.44 % (1800050)Instructions burned: 434 (million)
% 157.20/23.44 % (1800054)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=296021241:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2894 on theBenchmark for (2894ds/2942Mi)
% 157.20/23.44 % (1800055)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=791870762:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2893 on theBenchmark for (2893ds/6922Mi)
% 157.20/23.44 % (1800048)Instruction limit reached!
% 157.20/23.44 % (1800048)------------------------------
% 157.20/23.44 % (1800048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.20/23.44 % (1800048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800048)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800048)Termination reason: Instruction limit
% 172.25/25.53 % (1800048)Termination phase: Saturation
% 172.25/25.53 % (1800048)Time elapsed: 2.231 s
% 172.25/25.53 % (1800048)Peak memory usage: 139 MB
% 172.25/25.53 % (1800048)Instructions burned: 2088 (million)
% 172.25/25.53 % (1800054)Instruction limit reached!
% 172.25/25.53 % (1800054)------------------------------
% 172.25/25.53 % (1800054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.25/25.53 % (1800054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800054)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800054)Termination reason: Instruction limit
% 172.25/25.53 % (1800054)Termination phase: Saturation
% 172.25/25.53 % (1800054)Time elapsed: 1.597 s
% 172.25/25.53 % (1800054)Peak memory usage: 135 MB
% 172.25/25.53 % (1800054)Instructions burned: 2944 (million)
% 172.25/25.53 % (1800058)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1422037210:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2877 on theBenchmark for (2877ds/596Mi)
% 172.25/25.53 % (1800059)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1784616735:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2875 on theBenchmark for (2875ds/4123Mi)
% 172.25/25.53 % (1800058)Instruction limit reached!
% 172.25/25.53 % (1800058)------------------------------
% 172.25/25.53 % (1800058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.25/25.53 % (1800058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800058)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800058)Termination reason: Instruction limit
% 172.25/25.53 % (1800058)Termination phase: Saturation
% 172.25/25.53 % (1800058)Time elapsed: 0.557 s
% 172.25/25.53 % (1800058)Peak memory usage: 98 MB
% 172.25/25.53 % (1800058)Instructions burned: 597 (million)
% 172.25/25.53 % (1800062)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2826618670:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2868 on theBenchmark for (2868ds/16411Mi)
% 172.25/25.53 % (1800032)Instruction limit reached!
% 172.25/25.53 % (1800032)------------------------------
% 172.25/25.53 % (1800032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.25/25.53 % (1800032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800032)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800032)Termination reason: Instruction limit
% 172.25/25.53 % (1800032)Termination phase: Saturation
% 172.25/25.53 % (1800032)Time elapsed: 10.425 s
% 172.25/25.53 % (1800032)Peak memory usage: 176 MB
% 172.25/25.53 % (1800032)Instructions burned: 10308 (million)
% 172.25/25.53 % (1800059)Instruction limit reached!
% 172.25/25.53 % (1800059)------------------------------
% 172.25/25.53 % (1800059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.25/25.53 % (1800059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800059)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800059)Termination reason: Instruction limit
% 172.25/25.53 % (1800059)Termination phase: Saturation
% 172.25/25.53 % (1800059)Time elapsed: 2.400 s
% 172.25/25.53 % (1800059)Peak memory usage: 161 MB
% 172.25/25.53 % (1800059)Instructions burned: 4123 (million)
% 172.25/25.53 % (1800081)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1550685126:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2849 on theBenchmark for (2849ds/1670Mi)
% 172.25/25.53 % (1800082)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2099904352:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2848 on theBenchmark for (2848ds/1722Mi)
% 172.25/25.53 % (1800082)Instruction limit reached!
% 172.25/25.53 % (1800082)------------------------------
% 172.25/25.53 % (1800082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.25/25.53 % (1800082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.25/25.53 % (1800082)CaDiCaL version: 2.1.3
% 172.25/25.53 % (1800082)Termination reason: Instruction limit
% 172.25/25.53 % (1800082)Termination phase: Saturation
% 172.25/25.53 % (1800082)Time elapsed: 1.013 s
% 172.25/25.53 % (1800082)Peak memory usage: 134 MB
% 172.25/25.53 % (1800082)Instructions burned: 1724 (million)
% 172.25/25.53 % (1800085)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=763420896:cts=off:cond=on:i=9530:bs=on:fsd=on_2836 on theBenchmark for (2836ds/9530Mi)
% 198.05/29.13 % (1800081)Instruction limit reached!
% 198.05/29.13 % (1800081)------------------------------
% 198.05/29.13 % (1800081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.05/29.13 % (1800081)CaDiCaL version: 2.1.3
% 198.05/29.13 % (1800081)Termination reason: Instruction limit
% 198.05/29.13 % (1800081)Termination phase: Saturation
% 198.05/29.13 % (1800081)Time elapsed: 1.822 s
% 198.05/29.13 % (1800081)Peak memory usage: 136 MB
% 198.05/29.13 % (1800081)Instructions burned: 1670 (million)
% 198.05/29.13 % (1800055)Instruction limit reached!
% 198.05/29.13 % (1800055)------------------------------
% 198.05/29.13 % (1800055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.05/29.13 % (1800055)CaDiCaL version: 2.1.3
% 198.05/29.13 % (1800055)Termination reason: Instruction limit
% 198.05/29.13 % (1800055)Termination phase: Saturation
% 198.05/29.13 % (1800055)Time elapsed: 6.554 s
% 198.05/29.13 % (1800055)Peak memory usage: 187 MB
% 198.05/29.13 % (1800055)Instructions burned: 6923 (million)
% 198.05/29.13 % (1800087)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=399645928:st=2:i=4495:sd=10:ss=included_2828 on theBenchmark for (2828ds/4495Mi)
% 198.05/29.13 % (1800089)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=978722878:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2825 on theBenchmark for (2825ds/4920Mi)
% 198.05/29.13 % (1800085)Instruction limit reached!
% 198.05/29.13 % (1800085)------------------------------
% 198.05/29.13 % (1800085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.05/29.13 % (1800085)CaDiCaL version: 2.1.3
% 198.05/29.13 % (1800085)Termination reason: Instruction limit
% 198.05/29.13 % (1800085)Termination phase: Saturation
% 198.05/29.13 % (1800085)Time elapsed: 4.709 s
% 198.05/29.13 % (1800085)Peak memory usage: 173 MB
% 198.05/29.13 % (1800085)Instructions burned: 9531 (million)
% 198.05/29.13 % (1800152)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1780109240:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2786 on theBenchmark for (2786ds/2083Mi)
% 198.05/29.13 % (1800087)Instruction limit reached!
% 198.05/29.13 % (1800087)------------------------------
% 198.05/29.13 % (1800087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.05/29.13 % (1800087)CaDiCaL version: 2.1.3
% 198.05/29.13 % (1800087)Termination reason: Instruction limit
% 198.05/29.13 % (1800087)Termination phase: Saturation
% 198.05/29.13 % (1800087)Time elapsed: 4.139 s
% 198.05/29.13 % (1800087)Peak memory usage: 157 MB
% 198.05/29.13 % (1800087)Instructions burned: 4495 (million)
% 198.05/29.13 % (1800187)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2412786464:i=4629:av=off:gsp=on_2783 on theBenchmark for (2783ds/4629Mi)
% 198.05/29.13 % (1800089)Instruction limit reached!
% 198.05/29.13 % (1800089)------------------------------
% 198.05/29.13 % (1800089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.05/29.13 % (1800089)CaDiCaL version: 2.1.3
% 198.05/29.13 % (1800089)Termination reason: Instruction limit
% 198.05/29.13 % (1800089)Termination phase: Saturation
% 198.05/29.13 % (1800089)Time elapsed: 4.146 s
% 198.05/29.13 % (1800089)Peak memory usage: 164 MB
% 198.05/29.13 % (1800089)Instructions burned: 4921 (million)
% 198.05/29.13 % (1800246)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2868488981:i=1258:av=off_2780 on theBenchmark for (2780ds/1258Mi)
% 198.05/29.13 % (1800152)Instruction limit reached!
% 198.05/29.13 % (1800152)------------------------------
% 198.05/29.13 % (1800152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.05/29.13 % (1800152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800152)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800152)Termination reason: Instruction limit
% 218.61/32.13 % (1800152)Termination phase: Saturation
% 218.61/32.13 % (1800152)Time elapsed: 0.700 s
% 218.61/32.13 % (1800152)Peak memory usage: 136 MB
% 218.61/32.13 % (1800152)Instructions burned: 2085 (million)
% 218.61/32.13 % (1800253)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=831087344:i=7343:av=off:ss=included_2778 on theBenchmark for (2778ds/7343Mi)
% 218.61/32.13 % (1800187)Refutation not found, incomplete strategy
% 218.61/32.13 % (1800187)------------------------------
% 218.61/32.13 % (1800187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.61/32.13 % (1800187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800187)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800187)Termination reason: Refutation not found, incomplete strategy
% 218.61/32.13 % (1800187)Time elapsed: 0.589 s
% 218.61/32.13 % (1800187)Peak memory usage: 127 MB
% 218.61/32.13 % (1800187)Instructions burned: 892 (million)
% 218.61/32.13 % (1800187)------------------------------
% 218.61/32.13 % (1800187)------------------------------
% 218.61/32.13 % (1800255)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2257974588:i=1325:sd=2:ss=axioms:sgt=16_2773 on theBenchmark for (2773ds/1325Mi)
% 218.61/32.13 % (1800255)Refutation not found, incomplete strategy
% 218.61/32.13 % (1800255)------------------------------
% 218.61/32.13 % (1800255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.61/32.13 % (1800255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800255)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800255)Termination reason: Refutation not found, incomplete strategy
% 218.61/32.13 % (1800255)Time elapsed: 0.001 s
% 218.61/32.13 % (1800255)Peak memory usage: 87 MB
% 218.61/32.13 % (1800246)Instruction limit reached!
% 218.61/32.13 % (1800246)------------------------------
% 218.61/32.13 % (1800246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.61/32.13 % (1800246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800246)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800246)Termination reason: Instruction limit
% 218.61/32.13 % (1800246)Termination phase: Saturation
% 218.61/32.13 % (1800246)Time elapsed: 0.757 s
% 218.61/32.13 % (1800246)Peak memory usage: 103 MB
% 218.61/32.13 % (1800246)Instructions burned: 1258 (million)
% 218.61/32.13 % (1800255)------------------------------
% 218.61/32.13 % (1800255)------------------------------
% 218.61/32.13 % (1800258)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2667851161:i=1489:sd=2:ep=R:ss=axioms_2771 on theBenchmark for (2771ds/1489Mi)
% 218.61/32.13 % (1800257)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3189130340:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2771 on theBenchmark for (2771ds/2646Mi)
% 218.61/32.13 % (1800258)Refutation not found, incomplete strategy
% 218.61/32.13 % (1800258)------------------------------
% 218.61/32.13 % (1800258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.61/32.13 % (1800258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800258)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800258)Termination reason: Refutation not found, incomplete strategy
% 218.61/32.13 % (1800258)Time elapsed: 0.348 s
% 218.61/32.13 % (1800258)Peak memory usage: 127 MB
% 218.61/32.13 % (1800258)Instructions burned: 892 (million)
% 218.61/32.13 % (1800258)------------------------------
% 218.61/32.13 % (1800258)------------------------------
% 218.61/32.13 % (1800261)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2180049964:i=1503_2764 on theBenchmark for (2764ds/1503Mi)
% 218.61/32.13 % (1800257)Instruction limit reached!
% 218.61/32.13 % (1800257)------------------------------
% 218.61/32.13 % (1800257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.61/32.13 % (1800257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.61/32.13 % (1800257)CaDiCaL version: 2.1.3
% 218.61/32.13 % (1800257)Termination reason: Instruction limit
% 218.61/32.13 % (1800257)Termination phase: Saturation
% 218.61/32.13 % (1800257)Time elapsed: 1.142 s
% 218.61/32.13 % (1800257)Peak memory usage: 136 MB
% 218.61/32.13 % (1800257)Instructions burned: 2648 (million)
% 218.61/32.13 % (1800261)Refutation not found, incomplete strategy
% 242.44/35.49 % (1800261)------------------------------
% 242.44/35.49 % (1800261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.44/35.49 % (1800261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.44/35.49 % (1800261)CaDiCaL version: 2.1.3
% 242.44/35.49 % (1800261)Termination reason: Refutation not found, incomplete strategy
% 242.44/35.49 % (1800261)Time elapsed: 0.592 s
% 242.44/35.49 % (1800261)Peak memory usage: 127 MB
% 242.44/35.49 % (1800261)Instructions burned: 889 (million)
% 242.44/35.49 % (1800263)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2661355683:i=13942:kws=frequency_2758 on theBenchmark for (2758ds/13942Mi)
% 242.44/35.49 % (1800261)------------------------------
% 242.44/35.49 % (1800261)------------------------------
% 242.44/35.49 % (1800265)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3317009591:i=3604:fsr=off:er=filter_2754 on theBenchmark for (2754ds/3604Mi)
% 242.44/35.49 % (1800062)Instruction limit reached!
% 242.44/35.49 % (1800062)------------------------------
% 242.44/35.49 % (1800062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.44/35.49 % (1800062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.44/35.49 % (1800062)CaDiCaL version: 2.1.3
% 242.44/35.49 % (1800062)Termination reason: Instruction limit
% 242.44/35.49 % (1800062)Termination phase: Saturation
% 242.44/35.49 % (1800062)Time elapsed: 12.763 s
% 242.44/35.49 % (1800062)Peak memory usage: 250 MB
% 242.44/35.49 % (1800062)Instructions burned: 16411 (million)
% 242.44/35.49 % (1800267)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=829461674:i=1876:sd=1:ss=included:sgt=32_2737 on theBenchmark for (2737ds/1876Mi)
% 242.44/35.49 % (1800253)Instruction limit reached!
% 242.44/35.49 % (1800253)------------------------------
% 242.44/35.49 % (1800253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.44/35.49 % (1800253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.44/35.49 % (1800253)CaDiCaL version: 2.1.3
% 242.44/35.49 % (1800253)Termination reason: Instruction limit
% 242.44/35.49 % (1800253)Termination phase: Saturation
% 242.44/35.49 % (1800253)Time elapsed: 4.241 s
% 242.44/35.49 % (1800253)Peak memory usage: 190 MB
% 242.44/35.49 % (1800253)Instructions burned: 7344 (million)
% 242.44/35.49 % (1800265)Instruction limit reached!
% 242.44/35.49 % (1800265)------------------------------
% 242.44/35.49 % (1800265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.44/35.49 % (1800265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.44/35.49 % (1800265)CaDiCaL version: 2.1.3
% 242.44/35.49 % (1800265)Termination reason: Instruction limit
% 242.44/35.49 % (1800265)Termination phase: Saturation
% 242.44/35.49 % (1800265)Time elapsed: 1.998 s
% 242.44/35.49 % (1800265)Peak memory usage: 154 MB
% 242.44/35.49 % (1800265)Instructions burned: 3604 (million)
% 242.44/35.49 % (1800269)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3242520941:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2734 on theBenchmark for (2734ds/1932Mi)
% 242.44/35.49 % (1800271)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=178101164:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2732 on theBenchmark for (2732ds/1980Mi)
% 242.44/35.49 % (1800267)Instruction limit reached!
% 242.44/35.49 % (1800267)------------------------------
% 242.44/35.49 % (1800267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.44/35.49 % (1800267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.44/35.49 % (1800267)CaDiCaL version: 2.1.3
% 242.44/35.49 % (1800267)Termination reason: Instruction limit
% 242.44/35.49 % (1800267)Termination phase: Saturation
% 242.44/35.49 % (1800267)Time elapsed: 1.139 s
% 242.44/35.49 % (1800267)Peak memory usage: 136 MB
% 242.44/35.49 % (1800267)Instructions burned: 1877 (million)
% 242.44/35.49 % (1800389)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=4193643515:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2724 on theBenchmark for (2724ds/3902Mi)
% 242.44/35.49 % (1800269)Instruction limit reached!
% 242.44/35.49 % (1800269)------------------------------
% 258.98/37.81 % (1800269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800269)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800269)Termination reason: Instruction limit
% 258.98/37.81 % (1800269)Termination phase: Saturation
% 258.98/37.81 % (1800269)Time elapsed: 1.147 s
% 258.98/37.81 % (1800269)Peak memory usage: 138 MB
% 258.98/37.81 % (1800269)Instructions burned: 1934 (million)
% 258.98/37.81 % (1800391)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2004509438:avsq=on:i=3916:aac=none:amm=off_2721 on theBenchmark for (2721ds/3916Mi)
% 258.98/37.81 % (1800271)Instruction limit reached!
% 258.98/37.81 % (1800271)------------------------------
% 258.98/37.81 % (1800271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800271)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800271)Termination reason: Instruction limit
% 258.98/37.81 % (1800271)Termination phase: Saturation
% 258.98/37.81 % (1800271)Time elapsed: 1.254 s
% 258.98/37.81 % (1800271)Peak memory usage: 134 MB
% 258.98/37.81 % (1800271)Instructions burned: 1982 (million)
% 258.98/37.81 % (1800405)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=315984665:cond=on:i=3940:av=off:er=known_2718 on theBenchmark for (2718ds/3940Mi)
% 258.98/37.81 % (1800389)Refutation not found, incomplete strategy
% 258.98/37.81 % (1800389)------------------------------
% 258.98/37.81 % (1800389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800389)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800389)Termination reason: Refutation not found, incomplete strategy
% 258.98/37.81 % (1800389)Time elapsed: 0.587 s
% 258.98/37.81 % (1800389)Peak memory usage: 127 MB
% 258.98/37.81 % (1800389)Instructions burned: 892 (million)
% 258.98/37.81 % (1800389)------------------------------
% 258.98/37.81 % (1800389)------------------------------
% 258.98/37.81 % (1800496)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=208791185:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2713 on theBenchmark for (2713ds/3980Mi)
% 258.98/37.81 % (1800263)Instruction limit reached!
% 258.98/37.81 % (1800263)------------------------------
% 258.98/37.81 % (1800263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800263)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800263)Termination reason: Instruction limit
% 258.98/37.81 % (1800263)Termination phase: Saturation
% 258.98/37.81 % (1800263)Time elapsed: 4.998 s
% 258.98/37.81 % (1800263)Peak memory usage: 243 MB
% 258.98/37.81 % (1800263)Instructions burned: 13943 (million)
% 258.98/37.81 % (1800537)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2012796981:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2706 on theBenchmark for (2706ds/2087Mi)
% 258.98/37.81 % (1800537)Instruction limit reached!
% 258.98/37.81 % (1800537)------------------------------
% 258.98/37.81 % (1800537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800537)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800537)Termination reason: Instruction limit
% 258.98/37.81 % (1800537)Termination phase: Saturation
% 258.98/37.81 % (1800537)Time elapsed: 1.029 s
% 258.98/37.81 % (1800537)Peak memory usage: 142 MB
% 258.98/37.81 % (1800537)Instructions burned: 2088 (million)
% 258.98/37.81 % (1800578)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=482698545:cts=off:cond=on:i=4272:bs=on:fsd=on_2694 on theBenchmark for (2694ds/4272Mi)
% 258.98/37.81 % (1800391)Instruction limit reached!
% 258.98/37.81 % (1800391)------------------------------
% 258.98/37.81 % (1800391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 258.98/37.81 % (1800391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 258.98/37.81 % (1800391)CaDiCaL version: 2.1.3
% 258.98/37.81 % (1800391)Termination reason: Instruction limit
% 294.25/43.70 % (1800391)Termination phase: Saturation
% 294.25/43.70 % (1800391)Time elapsed: 2.832 s
% 294.25/43.70 % (1800391)Peak memory usage: 117 MB
% 294.25/43.70 % (1800391)Instructions burned: 3917 (million)
% 294.25/43.70 % (1800646)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3567475601:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2691 on theBenchmark for (2691ds/2197Mi)
% 294.25/43.70 % (1800405)Instruction limit reached!
% 294.25/43.70 % (1800405)------------------------------
% 294.25/43.70 % (1800405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800405)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800405)Termination reason: Instruction limit
% 294.25/43.70 % (1800405)Termination phase: Saturation
% 294.25/43.70 % (1800405)Time elapsed: 2.939 s
% 294.25/43.70 % (1800405)Peak memory usage: 155 MB
% 294.25/43.70 % (1800405)Instructions burned: 3942 (million)
% 294.25/43.70 % (1800675)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2187489114:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2687 on theBenchmark for (2687ds/6508Mi)
% 294.25/43.70 % (1800496)Instruction limit reached!
% 294.25/43.70 % (1800496)------------------------------
% 294.25/43.70 % (1800496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800496)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800496)Termination reason: Instruction limit
% 294.25/43.70 % (1800496)Termination phase: Saturation
% 294.25/43.70 % (1800496)Time elapsed: 2.981 s
% 294.25/43.70 % (1800496)Peak memory usage: 153 MB
% 294.25/43.70 % (1800496)Instructions burned: 3980 (million)
% 294.25/43.70 % (1800708)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3481492827:i=2330:fgj=on:av=off:fsr=off_2682 on theBenchmark for (2682ds/2330Mi)
% 294.25/43.70 % (1800578)Instruction limit reached!
% 294.25/43.70 % (1800578)------------------------------
% 294.25/43.70 % (1800578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800578)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800578)Termination reason: Instruction limit
% 294.25/43.70 % (1800578)Termination phase: Saturation
% 294.25/43.70 % (1800578)Time elapsed: 1.411 s
% 294.25/43.70 % (1800578)Peak memory usage: 153 MB
% 294.25/43.70 % (1800578)Instructions burned: 4276 (million)
% 294.25/43.70 % (1800710)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1311478355:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2678 on theBenchmark for (2678ds/7592Mi)
% 294.25/43.70 % (1800646)Instruction limit reached!
% 294.25/43.70 % (1800646)------------------------------
% 294.25/43.70 % (1800646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800646)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800646)Termination reason: Instruction limit
% 294.25/43.70 % (1800646)Termination phase: Saturation
% 294.25/43.70 % (1800646)Time elapsed: 1.343 s
% 294.25/43.70 % (1800646)Peak memory usage: 140 MB
% 294.25/43.70 % (1800646)Instructions burned: 2198 (million)
% 294.25/43.70 % (1800712)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3687425737:i=2693:kws=precedence:ins=1:av=off_2676 on theBenchmark for (2676ds/2693Mi)
% 294.25/43.70 % (1800708)Instruction limit reached!
% 294.25/43.70 % (1800708)------------------------------
% 294.25/43.70 % (1800708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800708)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800708)Termination reason: Instruction limit
% 294.25/43.70 % (1800708)Termination phase: Saturation
% 294.25/43.70 % (1800708)Time elapsed: 1.433 s
% 294.25/43.70 % (1800708)Peak memory usage: 139 MB
% 294.25/43.70 % (1800708)Instructions burned: 2330 (million)
% 294.25/43.70 % (1800714)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1958587129:i=28651:sd=4:ss=included:sgt=64_2666 on theBenchmark for (2666ds/28651Mi)
% 294.25/43.70 % (1800712)Instruction limit reached!
% 294.25/43.70 % (1800712)------------------------------
% 294.25/43.70 % (1800712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800712)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800712)Termination reason: Instruction limit
% 294.25/43.70 % (1800712)Termination phase: Saturation
% 294.25/43.70 % (1800712)Time elapsed: 1.666 s
% 294.25/43.70 % (1800712)Peak memory usage: 145 MB
% 294.25/43.70 % (1800712)Instructions burned: 2693 (million)
% 294.25/43.70 % (1800716)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2299046656:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2657 on theBenchmark for (2657ds/2700Mi)
% 294.25/43.70 % (1800710)Instruction limit reached!
% 294.25/43.70 % (1800710)------------------------------
% 294.25/43.70 % (1800710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800710)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800710)Termination reason: Instruction limit
% 294.25/43.70 % (1800710)Termination phase: Saturation
% 294.25/43.70 % (1800710)Time elapsed: 2.378 s
% 294.25/43.70 % (1800710)Peak memory usage: 111 MB
% 294.25/43.70 % (1800710)Instructions burned: 7596 (million)
% 294.25/43.70 % (1800718)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=875476062:i=3196:nm=4_2653 on theBenchmark for (2653ds/3196Mi)
% 294.25/43.70 % (1800718)Refutation not found, incomplete strategy
% 294.25/43.70 % (1800718)------------------------------
% 294.25/43.70 % (1800718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800718)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800718)Termination reason: Refutation not found, incomplete strategy
% 294.25/43.70 % (1800718)Time elapsed: 0.323 s
% 294.25/43.70 % (1800718)Peak memory usage: 127 MB
% 294.25/43.70 % (1800718)Instructions burned: 888 (million)
% 294.25/43.70 % (1800718)------------------------------
% 294.25/43.70 % (1800718)------------------------------
% 294.25/43.70 % (1800675)Instruction limit reached!
% 294.25/43.70 % (1800675)------------------------------
% 294.25/43.70 % (1800675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800675)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800675)Termination reason: Instruction limit
% 294.25/43.70 % (1800675)Termination phase: Saturation
% 294.25/43.70 % (1800675)Time elapsed: 3.824 s
% 294.25/43.70 % (1800675)Peak memory usage: 137 MB
% 294.25/43.70 % (1800675)Instructions burned: 6509 (million)
% 294.25/43.70 % (1800720)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=2347140709:cts=off:i=3254:av=off_2647 on theBenchmark for (2647ds/3254Mi)
% 294.25/43.70 % (1800721)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1463891556:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2647 on theBenchmark for (2647ds/3264Mi)
% 294.25/43.70 % (1800716)Instruction limit reached!
% 294.25/43.70 % (1800716)------------------------------
% 294.25/43.70 % (1800716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800716)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800716)Termination reason: Instruction limit
% 294.25/43.70 % (1800716)Termination phase: Saturation
% 294.25/43.70 % (1800716)Time elapsed: 1.680 s
% 294.25/43.70 % (1800716)Peak memory usage: 146 MB
% 294.25/43.70 % (1800716)Instructions burned: 2700 (million)
% 294.25/43.70 % (1800724)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=832619165:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2639 on theBenchmark for (2639ds/9708Mi)
% 294.25/43.70 % (1800720)Instruction limit reached!
% 294.25/43.70 % (1800720)------------------------------
% 294.25/43.70 % (1800720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800720)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800720)Termination reason: Instruction limit
% 294.25/43.70 % (1800720)Termination phase: Saturation
% 294.25/43.70 % (1800720)Time elapsed: 1.172 s
% 294.25/43.70 % (1800720)Peak memory usage: 145 MB
% 294.25/43.70 % (1800720)Instructions burned: 3254 (million)
% 294.25/43.70 % (1800726)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2487016136:i=21997:s2at=5:gtg=all_2634 on theBenchmark for (2634ds/21997Mi)
% 294.25/43.70 % (1800724)Refutation not found, incomplete strategy
% 294.25/43.70 % (1800724)------------------------------
% 294.25/43.70 % (1800724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800724)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800724)Termination reason: Refutation not found, incomplete strategy
% 294.25/43.70 % (1800724)Time elapsed: 0.583 s
% 294.25/43.70 % (1800724)Peak memory usage: 128 MB
% 294.25/43.70 % (1800724)Instructions burned: 886 (million)
% 294.25/43.70 % (1800724)------------------------------
% 294.25/43.70 % (1800724)------------------------------
% 294.25/43.70 % (1800728)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=768181330:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2629 on theBenchmark for (2629ds/7551Mi)
% 294.25/43.70 % (1800721)Instruction limit reached!
% 294.25/43.70 % (1800721)------------------------------
% 294.25/43.70 % (1800721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800721)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800721)Termination reason: Instruction limit
% 294.25/43.70 % (1800721)Termination phase: Saturation
% 294.25/43.70 % (1800721)Time elapsed: 2.156 s
% 294.25/43.70 % (1800721)Peak memory usage: 149 MB
% 294.25/43.70 % (1800721)Instructions burned: 3264 (million)
% 294.25/43.70 % (1800730)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=263953085:i=8924:sd=1:ss=included_2624 on theBenchmark for (2624ds/8924Mi)
% 294.25/43.70 % (1800730)Refutation not found, incomplete strategy
% 294.25/43.70 % (1800730)------------------------------
% 294.25/43.70 % (1800730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800730)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800730)Termination reason: Refutation not found, incomplete strategy
% 294.25/43.70 % (1800730)Time elapsed: 0.594 s
% 294.25/43.70 % (1800730)Peak memory usage: 128 MB
% 294.25/43.70 % (1800730)Instructions burned: 903 (million)
% 294.25/43.70 % (1800730)------------------------------
% 294.25/43.70 % (1800730)------------------------------
% 294.25/43.70 % (1800732)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=3813272396:i=9638:kws=frequency:bd=preordered_2614 on theBenchmark for (2614ds/9638Mi)
% 294.25/43.70 % (1800728)Instruction limit reached!
% 294.25/43.70 % (1800728)------------------------------
% 294.25/43.70 % (1800728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 294.25/43.70 % (1800728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 294.25/43.70 % (1800728)CaDiCaL version: 2.1.3
% 294.25/43.70 % (1800728)Termination reason: Instruction limit
% 294.25/43.70 % (1800728)Termination phase: Saturation
% 294.25/43.70 % (1800728)Time elapsed: 4.504 s
% 294.25/43.70 % (1800728)Peak memory usage: 137 MB
% 294.25/43.70 % (1800728)Instructions burned: 7553 (million)
% 294.25/43.70 % (1800736)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=1232832664:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2582 on theBenchmark for (2582ds/5177Mi)
% 294.25/43.70 % (1800726)First to succeed.
% 294.25/43.70 % (1800726)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1799974"
% 294.25/43.70 % (1800726)Refutation found. Thanks to Tanya!
% 294.25/43.70 % SZS status Unsatisfiable for theBenchmark
% 294.25/43.70 % SZS output start Proof for theBenchmark
% 294.25/43.70 fof(f1,axiom,(
% 294.25/43.70 ( ! [X0] : (axiom(implies(or(X0,X0),X0))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_2)).
% 294.25/43.70 fof(f2,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (axiom(implies(X0,or(X1,X0)))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_3)).
% 294.25/43.70 fof(f3,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (axiom(implies(or(X0,X1),or(X1,X0)))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_4)).
% 294.25/43.70 fof(f4,axiom,(
% 294.25/43.70 ( ! [X2,X0,X1] : (axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_5)).
% 294.25/43.70 fof(f5,axiom,(
% 294.25/43.70 ( ! [X2,X0,X1] : (axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_6)).
% 294.25/43.70 fof(f6,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (implies(X0,X1) = or(not(X0),X1)) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',implies_definition)).
% 294.25/43.70 fof(f7,axiom,(
% 294.25/43.70 ( ! [X0] : (~axiom(X0) | theorem(X0)) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_1)).
% 294.25/43.70 fof(f8,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(X0) | ~theorem(implies(X1,X0)) | ~theorem(X1)) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_2)).
% 294.25/43.70 fof(f9,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (and(X0,X1) = not(or(not(X0),not(X1)))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_defn)).
% 294.25/43.70 fof(f10,axiom,(
% 294.25/43.70 ( ! [X0,X1] : (equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0))) )),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equivalent_defn)).
% 294.25/43.70 fof(f11,negated_conjecture,(
% 294.25/43.70 ~theorem(equivalent(implies(p,equivalent(q,r)),equivalent(implies(p,q),implies(p,r))))),
% 294.25/43.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this)).
% 294.25/43.70 fof(f12,plain,(
% 294.25/43.70 ( ! [X0,X1] : (equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0))))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f10,f9,f6,f6])).
% 294.25/43.70 fof(f13,plain,(
% 294.25/43.70 ( ! [X0] : (axiom(or(not(or(X0,X0)),X0))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f1,f6])).
% 294.25/43.70 fof(f14,plain,(
% 294.25/43.70 ( ! [X0,X1] : (axiom(or(not(X0),or(X1,X0)))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f2,f6])).
% 294.25/43.70 fof(f15,plain,(
% 294.25/43.70 ( ! [X0,X1] : (axiom(or(not(or(X0,X1)),or(X1,X0)))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f3,f6])).
% 294.25/43.70 fof(f16,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2))))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f4,f6])).
% 294.25/43.70 fof(f17,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1))))) )),
% 294.25/43.70 inference(definition_unfolding,[],[f5,f6,f6,f6])).
% 294.25/43.70 fof(f18,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(not(X1),X0)) | theorem(X0) | ~theorem(X1)) )),
% 294.25/43.70 inference(definition_unfolding,[],[f8,f6])).
% 294.25/43.70 fof(f19,plain,(
% 294.25/43.70 ~theorem(not(or(not(or(not(or(not(p),not(or(not(or(not(q),r)),not(or(not(r),q)))))),not(or(not(or(not(or(not(p),q)),or(not(p),r))),not(or(not(or(not(p),r)),or(not(p),q))))))),not(or(not(not(or(not(or(not(or(not(p),q)),or(not(p),r))),not(or(not(or(not(p),r)),or(not(p),q)))))),or(not(p),not(or(not(or(not(q),r)),not(or(not(r),q))))))))))),
% 294.25/43.70 inference(definition_unfolding,[],[f11,f12,f6,f12,f12,f6,f6])).
% 294.25/43.70 fof(f20,definition,(
% 294.25/43.70 sF0 = not(p)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 294.25/43.70 fof(f21,plain,(
% 294.25/43.70 not(p) = sF0),
% 294.25/43.70 inference(reorient_equations,[],[f20])).
% 294.25/43.70 fof(f22,definition,(
% 294.25/43.70 sF1 = not(q)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 294.25/43.70 fof(f23,plain,(
% 294.25/43.70 not(q) = sF1),
% 294.25/43.70 inference(reorient_equations,[],[f22])).
% 294.25/43.70 fof(f24,definition,(
% 294.25/43.70 sF2 = or(sF1,r)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 294.25/43.70 fof(f25,plain,(
% 294.25/43.70 or(sF1,r) = sF2),
% 294.25/43.70 inference(reorient_equations,[],[f24])).
% 294.25/43.70 fof(f26,definition,(
% 294.25/43.70 sF3 = not(sF2)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 294.25/43.70 fof(f27,plain,(
% 294.25/43.70 not(sF2) = sF3),
% 294.25/43.70 inference(reorient_equations,[],[f26])).
% 294.25/43.70 fof(f28,definition,(
% 294.25/43.70 sF4 = not(r)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 294.25/43.70 fof(f29,plain,(
% 294.25/43.70 not(r) = sF4),
% 294.25/43.70 inference(reorient_equations,[],[f28])).
% 294.25/43.70 fof(f30,definition,(
% 294.25/43.70 sF5 = or(sF4,q)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 294.25/43.70 fof(f31,plain,(
% 294.25/43.70 or(sF4,q) = sF5),
% 294.25/43.70 inference(reorient_equations,[],[f30])).
% 294.25/43.70 fof(f32,definition,(
% 294.25/43.70 sF6 = not(sF5)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 294.25/43.70 fof(f33,plain,(
% 294.25/43.70 not(sF5) = sF6),
% 294.25/43.70 inference(reorient_equations,[],[f32])).
% 294.25/43.70 fof(f34,definition,(
% 294.25/43.70 sF7 = or(sF3,sF6)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 294.25/43.70 fof(f35,plain,(
% 294.25/43.70 or(sF3,sF6) = sF7),
% 294.25/43.70 inference(reorient_equations,[],[f34])).
% 294.25/43.70 fof(f36,definition,(
% 294.25/43.70 sF8 = not(sF7)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 294.25/43.70 fof(f37,plain,(
% 294.25/43.70 not(sF7) = sF8),
% 294.25/43.70 inference(reorient_equations,[],[f36])).
% 294.25/43.70 fof(f38,definition,(
% 294.25/43.70 sF9 = or(sF0,sF8)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 294.25/43.70 fof(f39,plain,(
% 294.25/43.70 or(sF0,sF8) = sF9),
% 294.25/43.70 inference(reorient_equations,[],[f38])).
% 294.25/43.70 fof(f40,definition,(
% 294.25/43.70 sF10 = not(sF9)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 294.25/43.70 fof(f41,plain,(
% 294.25/43.70 not(sF9) = sF10),
% 294.25/43.70 inference(reorient_equations,[],[f40])).
% 294.25/43.70 fof(f42,definition,(
% 294.25/43.70 sF11 = or(sF0,q)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 294.25/43.70 fof(f43,plain,(
% 294.25/43.70 or(sF0,q) = sF11),
% 294.25/43.70 inference(reorient_equations,[],[f42])).
% 294.25/43.70 fof(f44,definition,(
% 294.25/43.70 sF12 = not(sF11)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 294.25/43.70 fof(f45,plain,(
% 294.25/43.70 not(sF11) = sF12),
% 294.25/43.70 inference(reorient_equations,[],[f44])).
% 294.25/43.70 fof(f46,definition,(
% 294.25/43.70 sF13 = or(sF0,r)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 294.25/43.70 fof(f47,plain,(
% 294.25/43.70 or(sF0,r) = sF13),
% 294.25/43.70 inference(reorient_equations,[],[f46])).
% 294.25/43.70 fof(f48,definition,(
% 294.25/43.70 sF14 = or(sF12,sF13)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 294.25/43.70 fof(f49,plain,(
% 294.25/43.70 or(sF12,sF13) = sF14),
% 294.25/43.70 inference(reorient_equations,[],[f48])).
% 294.25/43.70 fof(f50,definition,(
% 294.25/43.70 sF15 = not(sF14)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 294.25/43.70 fof(f51,plain,(
% 294.25/43.70 not(sF14) = sF15),
% 294.25/43.70 inference(reorient_equations,[],[f50])).
% 294.25/43.70 fof(f52,definition,(
% 294.25/43.70 sF16 = not(sF13)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 294.25/43.70 fof(f53,plain,(
% 294.25/43.70 not(sF13) = sF16),
% 294.25/43.70 inference(reorient_equations,[],[f52])).
% 294.25/43.70 fof(f54,definition,(
% 294.25/43.70 sF17 = or(sF16,sF11)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 294.25/43.70 fof(f55,plain,(
% 294.25/43.70 or(sF16,sF11) = sF17),
% 294.25/43.70 inference(reorient_equations,[],[f54])).
% 294.25/43.70 fof(f56,definition,(
% 294.25/43.70 sF18 = not(sF17)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 294.25/43.70 fof(f57,plain,(
% 294.25/43.70 not(sF17) = sF18),
% 294.25/43.70 inference(reorient_equations,[],[f56])).
% 294.25/43.70 fof(f58,definition,(
% 294.25/43.70 sF19 = or(sF15,sF18)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 294.25/43.70 fof(f59,plain,(
% 294.25/43.70 or(sF15,sF18) = sF19),
% 294.25/43.70 inference(reorient_equations,[],[f58])).
% 294.25/43.70 fof(f60,definition,(
% 294.25/43.70 sF20 = not(sF19)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 294.25/43.70 fof(f61,plain,(
% 294.25/43.70 not(sF19) = sF20),
% 294.25/43.70 inference(reorient_equations,[],[f60])).
% 294.25/43.70 fof(f62,definition,(
% 294.25/43.70 sF21 = or(sF10,sF20)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 294.25/43.70 fof(f63,plain,(
% 294.25/43.70 or(sF10,sF20) = sF21),
% 294.25/43.70 inference(reorient_equations,[],[f62])).
% 294.25/43.70 fof(f64,definition,(
% 294.25/43.70 sF22 = not(sF21)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 294.25/43.70 fof(f65,plain,(
% 294.25/43.70 not(sF21) = sF22),
% 294.25/43.70 inference(reorient_equations,[],[f64])).
% 294.25/43.70 fof(f66,definition,(
% 294.25/43.70 sF23 = not(sF20)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 294.25/43.70 fof(f67,plain,(
% 294.25/43.70 not(sF20) = sF23),
% 294.25/43.70 inference(reorient_equations,[],[f66])).
% 294.25/43.70 fof(f68,definition,(
% 294.25/43.70 sF24 = or(sF23,sF9)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 294.25/43.70 fof(f69,plain,(
% 294.25/43.70 or(sF23,sF9) = sF24),
% 294.25/43.70 inference(reorient_equations,[],[f68])).
% 294.25/43.70 fof(f70,definition,(
% 294.25/43.70 sF25 = not(sF24)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 294.25/43.70 fof(f71,plain,(
% 294.25/43.70 not(sF24) = sF25),
% 294.25/43.70 inference(reorient_equations,[],[f70])).
% 294.25/43.70 fof(f72,definition,(
% 294.25/43.70 sF26 = or(sF22,sF25)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 294.25/43.70 fof(f73,plain,(
% 294.25/43.70 or(sF22,sF25) = sF26),
% 294.25/43.70 inference(reorient_equations,[],[f72])).
% 294.25/43.70 fof(f74,definition,(
% 294.25/43.70 sF27 = not(sF26)),
% 294.25/43.70 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 294.25/43.70 fof(f75,plain,(
% 294.25/43.70 not(sF26) = sF27),
% 294.25/43.70 inference(reorient_equations,[],[f74])).
% 294.25/43.70 fof(f76,plain,(
% 294.25/43.70 ~theorem(sF27)),
% 294.25/43.70 inference(definition_folding,[],[f19,f75,f73,f71,f69,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21,f67,f61,f59,f57,f55,f43,f21,f53,f47,f21,f51,f49,f47,f21,f45,f43,f21,f65,f63,f61,f59,f57,f55,f43,f21,f53,f47,f21,f51,f49,f47,f21,f45,f43,f21,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21])).
% 294.25/43.70 fof(f77,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2))))) )),
% 294.25/43.70 inference(resolution,[],[f16,f7])).
% 294.25/43.70 fof(f78,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (~theorem(or(X1,or(X0,X2))) | theorem(or(X0,or(X1,X2)))) )),
% 294.25/43.70 inference(resolution,[],[f77,f18])).
% 294.25/43.70 fof(f80,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1))))) )),
% 294.25/43.70 inference(resolution,[],[f17,f7])).
% 294.25/43.70 fof(f81,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,X1)),or(X0,X2))) | ~theorem(or(not(X1),X2))) )),
% 294.25/43.70 inference(resolution,[],[f80,f18])).
% 294.25/43.70 fof(f82,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2))))) )),
% 294.25/43.70 inference(resolution,[],[f80,f78])).
% 294.25/43.70 fof(f89,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(not(or(X0,X1)),or(X1,X0)))) )),
% 294.25/43.70 inference(resolution,[],[f15,f7])).
% 294.25/43.70 fof(f90,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(X1,X0)) | theorem(or(X0,X1))) )),
% 294.25/43.70 inference(resolution,[],[f89,f18])).
% 294.25/43.70 fof(f91,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(X0,or(not(or(X1,X0)),X1)))) )),
% 294.25/43.70 inference(resolution,[],[f89,f78])).
% 294.25/43.70 fof(f92,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (~theorem(or(not(X0),X1)) | theorem(or(X2,X1)) | ~theorem(or(X2,X0))) )),
% 294.25/43.70 inference(resolution,[],[f81,f18])).
% 294.25/43.70 fof(f94,plain,(
% 294.25/43.70 ( ! [X2,X3,X0,X1] : (~theorem(or(X0,or(X2,or(X1,X3)))) | theorem(or(X0,or(X1,or(X2,X3))))) )),
% 294.25/43.70 inference(resolution,[],[f92,f77])).
% 294.25/43.70 fof(f96,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (~theorem(or(X0,or(X2,X1))) | theorem(or(X0,or(X1,X2)))) )),
% 294.25/43.70 inference(resolution,[],[f92,f89])).
% 294.25/43.70 fof(f97,plain,(
% 294.25/43.70 ( ! [X2,X3,X0,X1] : (~theorem(or(X0,or(X1,X3))) | theorem(or(X0,or(X1,X2))) | ~theorem(or(not(X3),X2))) )),
% 294.25/43.70 inference(resolution,[],[f92,f81])).
% 294.25/43.70 fof(f98,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF1,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,q))) )),
% 294.25/43.70 inference(superposition,[],[f92,f23])).
% 294.25/43.70 fof(f108,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(X0,X0)),X0))) )),
% 294.25/43.70 inference(resolution,[],[f13,f7])).
% 294.25/43.70 fof(f109,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(X0,or(X1,X1))) | theorem(or(X0,X1))) )),
% 294.25/43.70 inference(resolution,[],[f108,f92])).
% 294.25/43.70 fof(f115,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(not(or(X0,X1)),X0)) | ~theorem(or(not(X1),X0))) )),
% 294.25/43.70 inference(resolution,[],[f109,f81])).
% 294.25/43.70 fof(f117,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF10,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF9))) )),
% 294.25/43.70 inference(superposition,[],[f92,f41])).
% 294.25/43.70 fof(f125,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF16,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF13))) )),
% 294.25/43.70 inference(superposition,[],[f92,f53])).
% 294.25/43.70 fof(f140,plain,(
% 294.25/43.70 ( ! [X0] : (~theorem(or(sF22,X0)) | theorem(X0) | ~theorem(sF21)) )),
% 294.25/43.70 inference(superposition,[],[f18,f65])).
% 294.25/43.70 fof(f149,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF25,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF24))) )),
% 294.25/43.70 inference(superposition,[],[f92,f71])).
% 294.25/43.70 fof(f153,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF8,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF7))) )),
% 294.25/43.70 inference(superposition,[],[f92,f37])).
% 294.25/43.70 fof(f157,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF18,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF17))) )),
% 294.25/43.70 inference(superposition,[],[f92,f57])).
% 294.25/43.70 fof(f165,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(sF20,X0)) | theorem(or(X1,X0)) | ~theorem(or(X1,sF19))) )),
% 294.25/43.70 inference(superposition,[],[f92,f61])).
% 294.25/43.70 fof(f178,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(not(q),X0)),or(not(sF11),or(sF0,X0))))) )),
% 294.25/43.70 inference(superposition,[],[f80,f43])).
% 294.25/43.70 fof(f187,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(not(q),X0)),or(sF12,or(sF0,X0))))) )),
% 294.25/43.70 inference(forward_demodulation,[],[f178,f45])).
% 294.25/43.70 fof(f191,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(sF1,X0)),or(sF12,or(sF0,X0))))) )),
% 294.25/43.70 inference(forward_demodulation,[],[f187,f23])).
% 294.25/43.70 fof(f202,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(not(r),X0)),or(not(sF13),or(sF0,X0))))) )),
% 294.25/43.70 inference(superposition,[],[f80,f47])).
% 294.25/43.70 fof(f211,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(not(r),X0)),or(sF16,or(sF0,X0))))) )),
% 294.25/43.70 inference(forward_demodulation,[],[f202,f53])).
% 294.25/43.70 fof(f215,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(or(sF4,X0)),or(sF16,or(sF0,X0))))) )),
% 294.25/43.70 inference(forward_demodulation,[],[f211,f29])).
% 294.25/43.70 fof(f217,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(not(X0),or(X1,X0)))) )),
% 294.25/43.70 inference(resolution,[],[f14,f7])).
% 294.25/43.70 fof(f238,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(X0,or(X1,X2))) | ~theorem(or(X0,X2))) )),
% 294.25/43.70 inference(resolution,[],[f217,f92])).
% 294.25/43.70 fof(f239,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(X0,X1)) | ~theorem(X1)) )),
% 294.25/43.70 inference(resolution,[],[f217,f18])).
% 294.25/43.70 fof(f240,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(X0,or(not(X1),X1)))) )),
% 294.25/43.70 inference(resolution,[],[f217,f78])).
% 294.25/43.70 fof(f241,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(not(X0),X0))) )),
% 294.25/43.70 inference(resolution,[],[f217,f109])).
% 294.25/43.70 fof(f260,plain,(
% 294.25/43.70 theorem(or(not(r),sF13))),
% 294.25/43.70 inference(superposition,[],[f217,f47])).
% 294.25/43.70 fof(f261,plain,(
% 294.25/43.70 theorem(or(sF4,sF13))),
% 294.25/43.70 inference(forward_demodulation,[],[f260,f29])).
% 294.25/43.70 fof(f267,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(X0,not(X0)))) )),
% 294.25/43.70 inference(resolution,[],[f241,f90])).
% 294.25/43.70 fof(f349,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,or(X1,X2))),or(or(X0,X2),X1)))) )),
% 294.25/43.70 inference(resolution,[],[f96,f77])).
% 294.25/43.70 fof(f352,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,X1)),or(X2,X0))) | ~theorem(or(not(X1),X2))) )),
% 294.25/43.70 inference(resolution,[],[f96,f81])).
% 294.25/43.70 fof(f354,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(not(X0),or(X0,X1)))) )),
% 294.25/43.70 inference(resolution,[],[f96,f217])).
% 294.25/43.70 fof(f356,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(X0,or(X1,X2))) | ~theorem(or(X0,X1))) )),
% 294.25/43.70 inference(resolution,[],[f96,f238])).
% 294.25/43.70 fof(f376,plain,(
% 294.25/43.70 theorem(or(not(sF9),or(sF8,sF0)))),
% 294.25/43.70 inference(superposition,[],[f89,f39])).
% 294.25/43.70 fof(f379,plain,(
% 294.25/43.70 theorem(or(not(sF8),sF9))),
% 294.25/43.70 inference(superposition,[],[f217,f39])).
% 294.25/43.70 fof(f381,plain,(
% 294.25/43.70 theorem(or(sF10,or(sF8,sF0)))),
% 294.25/43.70 inference(forward_demodulation,[],[f376,f41])).
% 294.25/43.70 fof(f389,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(X1,or(X0,X2))) | ~theorem(or(X0,X1))) )),
% 294.25/43.70 inference(resolution,[],[f356,f78])).
% 294.25/43.70 fof(f393,plain,(
% 294.25/43.70 ( ! [X0] : (~theorem(or(X0,sF0)) | theorem(or(X0,sF13))) )),
% 294.25/43.70 inference(superposition,[],[f356,f47])).
% 294.25/43.70 fof(f412,plain,(
% 294.25/43.70 theorem(or(not(sF26),or(sF25,sF22)))),
% 294.25/43.70 inference(superposition,[],[f89,f73])).
% 294.25/43.70 fof(f418,plain,(
% 294.25/43.70 theorem(or(sF27,or(sF25,sF22)))),
% 294.25/43.70 inference(forward_demodulation,[],[f412,f75])).
% 294.25/43.70 fof(f438,plain,(
% 294.25/43.70 theorem(or(not(sF7),or(sF6,sF3)))),
% 294.25/43.70 inference(superposition,[],[f89,f35])).
% 294.25/43.70 fof(f444,plain,(
% 294.25/43.70 theorem(or(sF8,or(sF6,sF3)))),
% 294.25/43.70 inference(forward_demodulation,[],[f438,f37])).
% 294.25/43.70 fof(f464,plain,(
% 294.25/43.70 theorem(or(not(sF19),or(sF18,sF15)))),
% 294.25/43.70 inference(superposition,[],[f89,f59])).
% 294.25/43.70 fof(f467,plain,(
% 294.25/43.70 theorem(or(not(sF18),sF19))),
% 294.25/43.70 inference(superposition,[],[f217,f59])).
% 294.25/43.70 fof(f468,plain,(
% 294.25/43.70 ( ! [X0] : (~theorem(or(X0,sF18)) | theorem(or(X0,sF19))) )),
% 294.25/43.70 inference(superposition,[],[f238,f59])).
% 294.25/43.70 fof(f470,plain,(
% 294.25/43.70 theorem(or(sF20,or(sF18,sF15)))),
% 294.25/43.70 inference(forward_demodulation,[],[f464,f61])).
% 294.25/43.70 fof(f493,plain,(
% 294.25/43.70 theorem(or(not(sF20),sF21))),
% 294.25/43.70 inference(superposition,[],[f217,f63])).
% 294.25/43.70 fof(f496,plain,(
% 294.25/43.70 theorem(or(sF23,sF21))),
% 294.25/43.70 inference(forward_demodulation,[],[f493,f67])).
% 294.25/43.70 fof(f521,plain,(
% 294.25/43.70 theorem(or(not(sF14),or(sF13,sF12)))),
% 294.25/43.70 inference(superposition,[],[f89,f49])).
% 294.25/43.70 fof(f528,plain,(
% 294.25/43.70 theorem(or(sF15,or(sF13,sF12)))),
% 294.25/43.70 inference(forward_demodulation,[],[f521,f51])).
% 294.25/43.70 fof(f586,plain,(
% 294.25/43.70 theorem(or(not(sF9),sF24))),
% 294.25/43.70 inference(superposition,[],[f217,f69])).
% 294.25/43.70 fof(f587,plain,(
% 294.25/43.70 ( ! [X0] : (~theorem(or(X0,sF9)) | theorem(or(X0,sF24))) )),
% 294.25/43.70 inference(superposition,[],[f238,f69])).
% 294.25/43.70 fof(f588,plain,(
% 294.25/43.70 ( ! [X0] : (~theorem(or(X0,sF23)) | theorem(or(X0,sF24))) )),
% 294.25/43.70 inference(superposition,[],[f356,f69])).
% 294.25/43.70 fof(f589,plain,(
% 294.25/43.70 theorem(or(sF10,sF24))),
% 294.25/43.70 inference(forward_demodulation,[],[f586,f41])).
% 294.25/43.70 fof(f602,plain,(
% 294.25/43.70 theorem(or(p,sF0))),
% 294.25/43.70 inference(superposition,[],[f267,f21])).
% 294.25/43.70 fof(f612,plain,(
% 294.25/43.70 theorem(or(sF17,sF18))),
% 294.25/43.70 inference(superposition,[],[f267,f57])).
% 294.25/43.70 fof(f624,plain,(
% 294.25/43.70 theorem(or(sF25,or(sF27,sF22)))),
% 294.25/43.70 inference(resolution,[],[f418,f78])).
% 294.25/43.70 fof(f634,plain,(
% 294.25/43.70 ( ! [X2,X3,X0,X1] : (theorem(or(not(or(X0,or(X1,X2))),or(X1,X3))) | ~theorem(or(not(or(X0,X2)),X3))) )),
% 294.25/43.70 inference(resolution,[],[f97,f77])).
% 294.25/43.70 fof(f635,plain,(
% 294.25/43.70 ( ! [X2,X3,X0,X1] : (theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),X3))) | ~theorem(or(not(or(X2,X1)),X3))) )),
% 294.25/43.70 inference(resolution,[],[f97,f80])).
% 294.25/43.70 fof(f636,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,X1)),or(X1,X2))) | ~theorem(or(not(X0),X2))) )),
% 294.25/43.70 inference(resolution,[],[f97,f89])).
% 294.25/43.70 fof(f663,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(not(X0),X1)),or(X2,X1))) | ~theorem(or(X2,X0))) )),
% 294.25/43.70 inference(resolution,[],[f82,f18])).
% 294.25/43.70 fof(f753,plain,(
% 294.25/43.70 theorem(or(sF8,or(sF10,sF0)))),
% 294.25/43.70 inference(resolution,[],[f381,f78])).
% 294.25/43.70 fof(f767,plain,(
% 294.25/43.70 theorem(or(sF25,or(sF22,sF27)))),
% 294.25/43.70 inference(resolution,[],[f624,f96])).
% 294.25/43.70 fof(f782,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(X0,or(not(X0),X1)))) )),
% 294.25/43.70 inference(resolution,[],[f354,f78])).
% 294.25/43.70 fof(f786,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(sF1,or(q,X0)))) )),
% 294.25/43.70 inference(superposition,[],[f354,f23])).
% 294.25/43.70 fof(f787,plain,(
% 294.25/43.70 ( ! [X0] : (theorem(or(sF4,or(r,X0)))) )),
% 294.25/43.70 inference(superposition,[],[f354,f29])).
% 294.25/43.70 fof(f803,plain,(
% 294.25/43.70 theorem(or(not(sF0),sF9))),
% 294.25/43.70 inference(superposition,[],[f354,f39])).
% 294.25/43.70 fof(f807,plain,(
% 294.25/43.70 theorem(or(not(sF10),sF21))),
% 294.25/43.70 inference(superposition,[],[f354,f63])).
% 294.25/43.70 fof(f809,plain,(
% 294.25/43.70 theorem(or(not(sF15),sF19))),
% 294.25/43.70 inference(superposition,[],[f354,f59])).
% 294.25/43.70 fof(f849,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (~theorem(or(not(X0),X1)) | theorem(or(X2,X1)) | ~theorem(or(X0,X2))) )),
% 294.25/43.70 inference(resolution,[],[f636,f18])).
% 294.25/43.70 fof(f853,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(not(or(X0,X1)),X1)) | ~theorem(or(not(X0),X1))) )),
% 294.25/43.70 inference(resolution,[],[f636,f109])).
% 294.25/43.70 fof(f891,plain,(
% 294.25/43.70 ( ! [X2,X0,X1] : (~theorem(or(X2,or(X0,X1))) | theorem(or(X2,X1)) | ~theorem(or(not(X0),X1))) )),
% 294.25/43.70 inference(resolution,[],[f853,f92])).
% 294.25/43.70 fof(f892,plain,(
% 294.25/43.70 ( ! [X0,X1] : (~theorem(or(not(X0),X1)) | theorem(X1) | ~theorem(or(X0,X1))) )),
% 294.25/43.70 inference(resolution,[],[f853,f18])).
% 294.25/43.70 fof(f936,plain,(
% 294.25/43.70 ( ! [X0,X1] : (theorem(or(X0,not(not(X1)))) | ~theorem(or(X1,X0))) )),
% 301.09/43.70 inference(resolution,[],[f849,f267])).
% 301.09/43.70 fof(f937,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(sF0,X0)) | theorem(or(X1,X0)) | ~theorem(or(p,X1))) )),
% 301.09/43.70 inference(superposition,[],[f849,f21])).
% 301.09/43.70 fof(f955,plain,(
% 301.09/43.70 theorem(or(sF18,or(sF20,sF15)))),
% 301.09/43.70 inference(resolution,[],[f470,f78])).
% 301.09/43.70 fof(f970,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (theorem(or(or(X0,X2),X1)) | ~theorem(or(X0,X1))) )),
% 301.09/43.70 inference(resolution,[],[f389,f90])).
% 301.09/43.70 fof(f986,plain,(
% 301.09/43.70 ( ! [X2,X3,X0,X1] : (~theorem(or(X2,or(not(X1),X3))) | theorem(or(X2,or(X0,X3))) | ~theorem(or(X0,X1))) )),
% 301.09/43.70 inference(resolution,[],[f663,f92])).
% 301.09/43.70 fof(f1002,plain,(
% 301.09/43.70 ( ! [X0,X1] : (theorem(or(not(or(sF15,X0)),or(X1,X0))) | ~theorem(or(X1,sF14))) )),
% 301.09/43.70 inference(superposition,[],[f663,f51])).
% 301.09/43.70 fof(f1058,plain,(
% 301.09/43.70 ( ! [X2,X3,X0,X1] : (~theorem(or(not(or(X0,X1)),X2)) | theorem(or(X3,X2)) | ~theorem(or(X0,or(X3,X1)))) )),
% 301.09/43.70 inference(resolution,[],[f634,f18])).
% 301.09/43.70 fof(f1097,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X2,or(X0,X1))) | theorem(or(X0,X1)) | ~theorem(or(not(X2),X1))) )),
% 301.09/43.70 inference(resolution,[],[f1058,f853])).
% 301.09/43.70 fof(f1107,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(not(sF11),X0)) | theorem(or(X1,X0)) | ~theorem(or(sF0,or(X1,q)))) )),
% 301.09/43.70 inference(superposition,[],[f1058,f43])).
% 301.09/43.70 fof(f1110,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(not(sF2),X0)) | theorem(or(X1,X0)) | ~theorem(or(sF1,or(X1,r)))) )),
% 301.09/43.70 inference(superposition,[],[f1058,f25])).
% 301.09/43.70 fof(f1112,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(not(sF5),X0)) | theorem(or(X1,X0)) | ~theorem(or(sF4,or(X1,q)))) )),
% 301.09/43.70 inference(superposition,[],[f1058,f31])).
% 301.09/43.70 fof(f1114,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(not(sF14),X0)) | theorem(or(X1,X0)) | ~theorem(or(sF12,or(X1,sF13)))) )),
% 301.09/43.70 inference(superposition,[],[f1058,f49])).
% 301.09/43.70 fof(f1123,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(sF12,or(X1,sF13))) | theorem(or(X1,X0)) | ~theorem(or(sF15,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f1114,f51])).
% 301.09/43.70 fof(f1125,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(sF4,or(X1,q))) | theorem(or(X1,X0)) | ~theorem(or(sF6,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f1112,f33])).
% 301.09/43.70 fof(f1127,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(sF1,or(X1,r))) | theorem(or(X1,X0)) | ~theorem(or(sF3,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f1110,f27])).
% 301.09/43.70 fof(f1130,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(sF0,or(X1,q))) | theorem(or(X1,X0)) | ~theorem(or(sF12,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f1107,f45])).
% 301.09/43.70 fof(f1165,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,not(sF16))) | ~theorem(or(X0,sF13))) )),
% 301.09/43.70 inference(resolution,[],[f125,f267])).
% 301.09/43.70 fof(f1167,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,or(sF10,sF0))) | ~theorem(or(X0,sF7))) )),
% 301.09/43.70 inference(resolution,[],[f153,f753])).
% 301.09/43.70 fof(f1175,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,or(sF22,sF27))) | ~theorem(or(X0,sF24))) )),
% 301.09/43.70 inference(resolution,[],[f149,f767])).
% 301.09/43.70 fof(f1228,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,not(sF20))) | ~theorem(or(X0,sF19))) )),
% 301.09/43.70 inference(resolution,[],[f165,f267])).
% 301.09/43.70 fof(f1229,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(X0,sF19)) | theorem(or(X0,sF23))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f1228,f67])).
% 301.09/43.70 fof(f1235,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,or(sF20,sF15))) | ~theorem(or(X0,sF17))) )),
% 301.09/43.70 inference(resolution,[],[f955,f157])).
% 301.09/43.70 fof(f1280,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(or(X0,X1),X2)),or(X0,or(X2,X1))))) )),
% 301.09/43.70 inference(resolution,[],[f94,f89])).
% 301.09/43.70 fof(f1351,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(or(X0,X2),X1)) | theorem(or(X0,or(X1,X2)))) )),
% 301.09/43.70 inference(resolution,[],[f1280,f18])).
% 301.09/43.70 fof(f1511,plain,(
% 301.09/43.70 theorem(or(not(or(sF1,r)),or(sF12,sF13)))),
% 301.09/43.70 inference(superposition,[],[f191,f47])).
% 301.09/43.70 fof(f1513,plain,(
% 301.09/43.70 theorem(or(not(or(sF1,r)),sF14))),
% 301.09/43.70 inference(forward_demodulation,[],[f1511,f49])).
% 301.09/43.70 fof(f1515,plain,(
% 301.09/43.70 theorem(or(not(sF2),sF14))),
% 301.09/43.70 inference(forward_demodulation,[],[f1513,f25])).
% 301.09/43.70 fof(f1517,plain,(
% 301.09/43.70 theorem(or(sF3,sF14))),
% 301.09/43.70 inference(forward_demodulation,[],[f1515,f27])).
% 301.09/43.70 fof(f1541,plain,(
% 301.09/43.70 theorem(or(not(or(sF4,q)),or(sF16,sF11)))),
% 301.09/43.70 inference(superposition,[],[f215,f43])).
% 301.09/43.70 fof(f1544,plain,(
% 301.09/43.70 theorem(or(not(or(sF4,q)),sF17))),
% 301.09/43.70 inference(forward_demodulation,[],[f1541,f55])).
% 301.09/43.70 fof(f1546,plain,(
% 301.09/43.70 theorem(or(not(sF5),sF17))),
% 301.09/43.70 inference(forward_demodulation,[],[f1544,f31])).
% 301.09/43.70 fof(f1548,plain,(
% 301.09/43.70 theorem(or(sF6,sF17))),
% 301.09/43.70 inference(forward_demodulation,[],[f1546,f33])).
% 301.09/43.70 fof(f1704,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(sF22,or(X0,sF27))) | ~theorem(or(X0,sF24))) )),
% 301.09/43.70 inference(resolution,[],[f1175,f78])).
% 301.09/43.70 fof(f1718,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF10,sF24)) | theorem(or(X0,or(sF22,sF27))) | ~theorem(or(X0,sF9))) )),
% 301.09/43.70 inference(resolution,[],[f1175,f117])).
% 301.09/43.70 fof(f1728,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(X0,or(sF22,sF27))) | ~theorem(or(X0,sF9))) )),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f1718,f589])).
% 301.09/43.70 fof(f1732,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(sF22,or(X0,sF27))) | ~theorem(or(X0,sF9))) )),
% 301.09/43.70 inference(resolution,[],[f1728,f78])).
% 301.09/43.70 fof(f1760,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X1,or(X2,X0))) | theorem(or(X2,X1)) | ~theorem(or(not(X0),X1))) )),
% 301.09/43.70 inference(resolution,[],[f115,f1058])).
% 301.09/43.70 fof(f1860,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (theorem(or(X2,or(X1,X0))) | ~theorem(or(X0,X1))) )),
% 301.09/43.70 inference(resolution,[],[f239,f96])).
% 301.09/43.70 fof(f2421,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X2,or(X0,X1))) | theorem(or(X0,X1)) | ~theorem(or(not(X2),X0))) )),
% 301.09/43.70 inference(resolution,[],[f892,f356])).
% 301.09/43.70 fof(f2555,plain,(
% 301.09/43.70 theorem(or(not(sF0),sF24))),
% 301.09/43.70 inference(resolution,[],[f803,f587])).
% 301.09/43.70 fof(f2761,plain,(
% 301.09/43.70 ( ! [X2,X3,X0,X1] : (~theorem(or(not(or(X0,X1)),X2)) | theorem(or(not(or(X0,X3)),X2)) | ~theorem(or(not(X3),X1))) )),
% 301.09/43.70 inference(resolution,[],[f635,f18])).
% 301.09/43.70 fof(f2842,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (theorem(or(not(or(X0,X1)),X2)) | ~theorem(or(not(X1),X2)) | ~theorem(or(not(X0),X2))) )),
% 301.09/43.70 inference(resolution,[],[f2761,f853])).
% 301.09/43.70 fof(f2931,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(not(X2),X1)) | ~theorem(or(not(X0),X1)) | theorem(X1) | ~theorem(or(X2,X0))) )),
% 301.09/43.70 inference(resolution,[],[f2842,f18])).
% 301.09/43.70 fof(f2972,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(sF11),X0)) | ~theorem(or(not(q),X0)) | ~theorem(or(not(sF0),X0))) )),
% 301.09/43.70 inference(superposition,[],[f2842,f43])).
% 301.09/43.70 fof(f2981,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(sF17),X0)) | ~theorem(or(not(sF11),X0)) | ~theorem(or(not(sF16),X0))) )),
% 301.09/43.70 inference(superposition,[],[f2842,f55])).
% 301.09/43.70 fof(f2986,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(sF18,X0)) | ~theorem(or(not(sF11),X0)) | ~theorem(or(not(sF16),X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f2981,f57])).
% 301.09/43.70 fof(f2995,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(sF12,X0)) | ~theorem(or(not(q),X0)) | ~theorem(or(not(sF0),X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f2972,f45])).
% 301.09/43.70 fof(f2997,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(not(sF16),X0)) | theorem(or(sF18,X0)) | ~theorem(or(sF12,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f2986,f45])).
% 301.09/43.70 fof(f3003,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(not(sF0),X0)) | theorem(or(sF12,X0)) | ~theorem(or(sF1,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f2995,f23])).
% 301.09/43.70 fof(f3028,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(not(X0),X1)) | theorem(or(X1,X2)) | ~theorem(or(X2,X0))) )),
% 301.09/43.70 inference(resolution,[],[f352,f18])).
% 301.09/43.70 fof(f3129,plain,(
% 301.09/43.70 ( ! [X0,X1] : (theorem(or(not(not(X0)),X1)) | ~theorem(or(X1,X0))) )),
% 301.09/43.70 inference(resolution,[],[f3028,f267])).
% 301.09/43.70 fof(f3241,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(sF20),X0)) | ~theorem(or(X0,sF19))) )),
% 301.09/43.70 inference(superposition,[],[f3129,f61])).
% 301.09/43.70 fof(f3246,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(X0,sF19)) | theorem(or(sF23,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f3241,f67])).
% 301.09/43.70 fof(f3342,plain,(
% 301.09/43.70 theorem(or(not(sF18),sF23))),
% 301.09/43.70 inference(resolution,[],[f467,f1229])).
% 301.09/43.70 fof(f3351,plain,(
% 301.09/43.70 theorem(or(not(sF18),sF24))),
% 301.09/43.70 inference(resolution,[],[f3342,f588])).
% 301.09/43.70 fof(f3356,plain,(
% 301.09/43.70 theorem(or(p,sF13))),
% 301.09/43.70 inference(resolution,[],[f602,f393])).
% 301.09/43.70 fof(f3724,plain,(
% 301.09/43.70 theorem(or(not(or(sF15,sF6)),sF7)) | ~theorem(or(sF3,sF14))),
% 301.09/43.70 inference(superposition,[],[f1002,f35])).
% 301.09/43.70 fof(f3734,plain,(
% 301.09/43.70 theorem(or(not(or(sF15,sF6)),sF7))),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f3724,f1517])).
% 301.09/43.70 fof(f4265,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X1,or(X2,X0))) | theorem(or(X0,or(X1,X2)))) )),
% 301.09/43.70 inference(resolution,[],[f91,f986])).
% 301.09/43.70 fof(f4641,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(X0,or(sF15,sF6))) | theorem(or(X0,sF7))) )),
% 301.09/43.70 inference(resolution,[],[f3734,f92])).
% 301.09/43.70 fof(f4659,plain,(
% 301.09/43.70 theorem(or(not(sF15),sF7))),
% 301.09/43.70 inference(resolution,[],[f4641,f354])).
% 301.09/43.70 fof(f4763,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X0,or(X2,X1))) | theorem(or(or(X0,X1),X2))) )),
% 301.09/43.70 inference(resolution,[],[f349,f18])).
% 301.09/43.70 fof(f4807,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (theorem(or(or(X0,X1),X2)) | ~theorem(or(X1,X2))) )),
% 301.09/43.70 inference(resolution,[],[f4763,f1860])).
% 301.09/43.70 fof(f4976,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF6,X0)) | theorem(or(sF7,X0))) )),
% 301.09/43.70 inference(superposition,[],[f4807,f35])).
% 301.09/43.70 fof(f4978,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF20,X0)) | theorem(or(sF21,X0))) )),
% 301.09/43.70 inference(superposition,[],[f4807,f63])).
% 301.09/43.70 fof(f4981,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF11,X0)) | theorem(or(sF17,X0))) )),
% 301.09/43.70 inference(superposition,[],[f4807,f55])).
% 301.09/43.70 fof(f5108,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(q),X0)) | ~theorem(or(sF12,X0))) )),
% 301.09/43.70 inference(resolution,[],[f1130,f240])).
% 301.09/43.70 fof(f5114,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF12,X0)) | theorem(or(sF1,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f5108,f23])).
% 301.09/43.70 fof(f5250,plain,(
% 301.09/43.70 theorem(or(not(sF15),sF23))),
% 301.09/43.70 inference(resolution,[],[f809,f1229])).
% 301.09/43.70 fof(f5259,plain,(
% 301.09/43.70 theorem(or(not(sF15),sF24))),
% 301.09/43.70 inference(resolution,[],[f5250,f588])).
% 301.09/43.70 fof(f5595,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF0,X0)) | theorem(or(sF11,X0))) )),
% 301.09/43.70 inference(superposition,[],[f970,f43])).
% 301.09/43.70 fof(f5601,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF10,X0)) | theorem(or(sF21,X0))) )),
% 301.09/43.70 inference(superposition,[],[f970,f63])).
% 301.09/43.70 fof(f5632,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(q),X0)) | ~theorem(or(sF6,X0))) )),
% 301.09/43.70 inference(resolution,[],[f1125,f240])).
% 301.09/43.70 fof(f5638,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF6,X0)) | theorem(or(sF1,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f5632,f23])).
% 301.09/43.70 fof(f5668,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(r),X0)) | ~theorem(or(sF3,X0))) )),
% 301.09/43.70 inference(resolution,[],[f1127,f240])).
% 301.09/43.70 fof(f5674,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF3,X0)) | theorem(or(sF4,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f5668,f29])).
% 301.09/43.70 fof(f5889,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(not(X0),or(X1,X2))) | theorem(or(X1,X2)) | ~theorem(or(X1,X0))) )),
% 301.09/43.70 inference(resolution,[],[f2931,f354])).
% 301.09/43.70 fof(f7602,plain,(
% 301.09/43.70 ( ! [X0,X1] : (theorem(or(not(not(X0)),X1)) | ~theorem(or(X0,X1))) )),
% 301.09/43.70 inference(resolution,[],[f936,f90])).
% 301.09/43.70 fof(f7676,plain,(
% 301.09/43.70 ( ! [X0,X1] : (~theorem(or(X0,or(X1,X1))) | theorem(or(not(not(X0)),X1))) )),
% 301.09/43.70 inference(resolution,[],[f7602,f109])).
% 301.09/43.70 fof(f7999,plain,(
% 301.09/43.70 theorem(or(sF17,sF19))),
% 301.09/43.70 inference(resolution,[],[f612,f468])).
% 301.09/43.70 fof(f8001,plain,(
% 301.09/43.70 theorem(or(sF23,sF17))),
% 301.09/43.70 inference(resolution,[],[f7999,f3246])).
% 301.09/43.70 fof(f8144,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(X0,sF13)) | theorem(or(sF0,X0)) | ~theorem(or(not(r),X0))) )),
% 301.09/43.70 inference(superposition,[],[f1760,f47])).
% 301.09/43.70 fof(f8161,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF4,X0)) | ~theorem(or(X0,sF13)) | theorem(or(sF0,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f8144,f29])).
% 301.09/43.70 fof(f16383,plain,(
% 301.09/43.70 theorem(or(sF12,or(sF22,sF27))) | ~theorem(or(sF1,or(sF22,sF27))) | ~theorem(or(not(sF0),sF24))),
% 301.09/43.70 inference(resolution,[],[f3003,f1175])).
% 301.09/43.70 fof(f16400,plain,(
% 301.09/43.70 theorem(or(sF12,or(sF22,sF27))) | ~theorem(or(sF1,or(sF22,sF27)))),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f16383,f2555])).
% 301.09/43.70 fof(f16705,plain,(
% 301.09/43.70 ( ! [X0] : (theorem(or(not(sF13),X0)) | ~theorem(or(sF15,X0))) )),
% 301.09/43.70 inference(resolution,[],[f1123,f240])).
% 301.09/43.70 fof(f16712,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF15,X0)) | theorem(or(sF16,X0))) )),
% 301.09/43.70 inference(forward_demodulation,[],[f16705,f53])).
% 301.09/43.70 fof(f18755,definition,(
% 301.09/43.70 spl28_7 <=> theorem(or(sF1,or(sF22,sF27)))),
% 301.09/43.70 introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition])).
% 301.09/43.70 fof(f18757,plain,(
% 301.09/43.70 ~theorem(or(sF1,or(sF22,sF27))) | spl28_7),
% 301.09/43.70 inference(avatar_component_clause,[],[f18755])).
% 301.09/43.70 fof(f18759,definition,(
% 301.09/43.70 spl28_8 <=> theorem(or(sF12,or(sF22,sF27)))),
% 301.09/43.70 introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition])).
% 301.09/43.70 fof(f18761,plain,(
% 301.09/43.70 theorem(or(sF12,or(sF22,sF27))) | ~spl28_8),
% 301.09/43.70 inference(avatar_component_clause,[],[f18759])).
% 301.09/43.70 fof(f18762,plain,(
% 301.09/43.70 ~spl28_7 | spl28_8),
% 301.09/43.70 inference(avatar_split_clause,[],[f16400,f18759,f18755])).
% 301.09/43.70 fof(f20114,plain,(
% 301.09/43.70 ( ! [X2,X0,X1] : (~theorem(or(X0,or(X1,X2))) | theorem(or(X0,X1)) | ~theorem(or(not(X2),X0))) )),
% 301.09/43.70 inference(resolution,[],[f5889,f352])).
% 301.09/43.70 fof(f21422,plain,(
% 301.09/43.70 theorem(or(sF7,or(sF20,sF15))) | ~theorem(or(sF6,sF17))),
% 301.09/43.70 inference(resolution,[],[f4976,f1235])).
% 301.09/43.70 fof(f21447,plain,(
% 301.09/43.70 theorem(or(sF7,or(sF20,sF15)))),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f21422,f1548])).
% 301.09/43.70 fof(f21458,plain,(
% 301.09/43.70 theorem(or(sF20,sF7)) | ~theorem(or(not(sF15),sF7))),
% 301.09/43.70 inference(resolution,[],[f21447,f1760])).
% 301.09/43.70 fof(f21466,plain,(
% 301.09/43.70 theorem(or(sF20,sF7))),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f21458,f4659])).
% 301.09/43.70 fof(f23363,definition,(
% 301.09/43.70 spl28_25 <=> theorem(sF21)),
% 301.09/43.70 introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition])).
% 301.09/43.70 fof(f23365,plain,(
% 301.09/43.70 ~theorem(sF21) | spl28_25),
% 301.09/43.70 inference(avatar_component_clause,[],[f23363])).
% 301.09/43.70 fof(f23367,definition,(
% 301.09/43.70 spl28_26 <=> ! [X0] : (~theorem(or(sF22,X0)) | theorem(X0))),
% 301.09/43.70 introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition])).
% 301.09/43.70 fof(f23368,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF22,X0)) | theorem(X0)) ) | ~spl28_26),
% 301.09/43.70 inference(avatar_component_clause,[],[f23367])).
% 301.09/43.70 fof(f23369,plain,(
% 301.09/43.70 ~spl28_25 | spl28_26),
% 301.09/43.70 inference(avatar_split_clause,[],[f140,f23367,f23363])).
% 301.09/43.70 fof(f24388,plain,(
% 301.09/43.70 theorem(or(sF21,or(sF10,sF0))) | ~theorem(or(sF20,sF7))),
% 301.09/43.70 inference(resolution,[],[f4978,f1167])).
% 301.09/43.70 fof(f24424,plain,(
% 301.09/43.70 theorem(or(sF21,or(sF10,sF0)))),
% 301.09/43.70 inference(forward_subsumption_resolution,[],[f24388,f21466])).
% 301.09/43.70 fof(f24428,plain,(
% 301.09/43.70 theorem(or(sF10,or(sF21,sF0)))),
% 301.09/43.70 inference(resolution,[],[f24424,f78])).
% 301.09/43.70 fof(f29482,definition,(
% 301.09/43.70 spl28_32 <=> theorem(or(sF0,sF21))),
% 301.09/43.70 introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition])).
% 301.09/43.70 fof(f29484,plain,(
% 301.09/43.70 theorem(or(sF0,sF21)) | ~spl28_32),
% 301.09/43.70 inference(avatar_component_clause,[],[f29482])).
% 301.09/43.70 fof(f47694,plain,(
% 301.09/43.70 ( ! [X0] : (~theorem(or(sF3,X0)) | theorem(or(q,X0))) )),
% 301.09/43.70 inference(resolution,[],[f786,f1127])).
% 301.09/43.70 fof(f49495,plain,(
% 301.09/43.70 theorem(or(sF21,sF0)) | ~theorem(or(not(sFTerminated
%------------------------------------------------------------------------------