%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM266_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.TvcA7DhBr4 true
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:23:23 PM UTC 2026
% Result : Theorem 33.07s 5.37s
% Output : Refutation 33.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 64 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 129 ( 92 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 1140 ( 61 ~; 53 |; 6 &;1014 @)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 8 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 47 ( 45 usr; 7 con; 0-5 aty)
% Number of variables : 199 ( 0 ^; 167 !; 32 ?; 199 :)
% Comments :
%------------------------------------------------------------------------------
thf(vEntry_type,type,
vEntry: $tType ).
thf(vQID_type,type,
vQID: $tType ).
thf(vLabel_type,type,
vLabel: $tType ).
thf(vAType_type,type,
vAType: $tType ).
thf(vExp_type,type,
vExp: $tType ).
thf(vQuestionnaire_type,type,
vQuestionnaire: $tType ).
thf(vMapConf_type,type,
vMapConf: $tType ).
thf(vATMap_type,type,
vATMap: $tType ).
thf(vAnsMap_type,type,
vAnsMap: $tType ).
thf(vQMap_type,type,
vQMap: $tType ).
thf(vOptQConf_type,type,
vOptQConf: $tType ).
thf(vQConf_type,type,
vQConf: $tType ).
thf(sk__309_type,type,
sk__309: vQID > vAnsMap > vQMap > vQMap ).
thf(vsomeQConf_type,type,
vsomeQConf: vQConf > vOptQConf ).
thf(sk__307_type,type,
sk__307: vQID > vAnsMap > vLabel > vAType > vQMap > vQuestionnaire ).
thf(vnoQConf_type,type,
vnoQConf: vOptQConf ).
thf(sk__4_type,type,
sk__4: vEntry > vQID ).
thf(sk__300_type,type,
sk__300: vQID > vAnsMap > vLabel > vAType > vQMap > vQMap ).
thf(sk__310_type,type,
sk__310: vQID > vAnsMap > vQMap > vQuestionnaire ).
thf(sk__299_type,type,
sk__299: vQID > vAnsMap > vLabel > vAType > vQMap > vAnsMap ).
thf(sk__314_type,type,
sk__314: vEntry ).
thf(vreduce_type,type,
vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf ).
thf(sk__303_type,type,
sk__303: vExp > vQID > vAnsMap > vAType > vQMap > vQMap ).
thf(sk__9_type,type,
sk__9: vEntry > vAType ).
thf(sk__5_type,type,
sk__5: vEntry > vAType ).
thf(sk__3_type,type,
sk__3: vEntry > vAType ).
thf(sk__type,type,
sk_: vEntry > vQID ).
thf(vtypeQM_type,type,
vtypeQM: vQMap > vATMap ).
thf(sk__40_type,type,
sk__40: vQConf > vQMap ).
thf(vdefquestion_type,type,
vdefquestion: vQID > vLabel > vAType > vEntry ).
thf(vptcheck_type,type,
vptcheck: vMapConf > vQuestionnaire > vMapConf > $o ).
thf(sk__6_type,type,
sk__6: vEntry > vExp ).
thf(sk__39_type,type,
sk__39: vQConf > vAnsMap ).
thf(sk__306_type,type,
sk__306: vQID > vAnsMap > vLabel > vAType > vQMap > vQMap ).
thf(sk__41_type,type,
sk__41: vQConf > vQuestionnaire ).
thf(sk__1_type,type,
sk__1: vEntry > vQID ).
thf(sk__24_type,type,
sk__24: vOptQConf > vQConf ).
thf(vMC_type,type,
vMC: vATMap > vATMap > vMapConf ).
thf(sk__312_type,type,
sk__312: vATMap ).
thf(sk__302_type,type,
sk__302: vExp > vQID > vAnsMap > vAType > vQMap > vAnsMap ).
thf(vqsingle_type,type,
vqsingle: vEntry > vQuestionnaire ).
thf(vquestion_type,type,
vquestion: vQID > vLabel > vAType > vEntry ).
thf(sk__304_type,type,
sk__304: vExp > vQID > vAnsMap > vAType > vQMap > vQuestionnaire ).
thf(visValue_type,type,
visValue: vQuestionnaire > $o ).
thf(vtypeAM_type,type,
vtypeAM: vAnsMap > vATMap ).
thf(sk__2_type,type,
sk__2: vEntry > vLabel ).
thf(vQC_type,type,
vQC: vAnsMap > vQMap > vQuestionnaire > vQConf ).
thf(sk__305_type,type,
sk__305: vQID > vAnsMap > vLabel > vAType > vQMap > vAnsMap ).
thf(sk__313_type,type,
sk__313: vATMap ).
thf(vask_type,type,
vask: vQID > vEntry ).
thf(sk__301_type,type,
sk__301: vQID > vAnsMap > vLabel > vAType > vQMap > vQuestionnaire ).
thf(vvalue_type,type,
vvalue: vQID > vAType > vExp > vEntry ).
thf(sk__315_type,type,
sk__315: vAnsMap ).
thf(sk__8_type,type,
sk__8: vEntry > vLabel ).
thf(sk__308_type,type,
sk__308: vQID > vAnsMap > vQMap > vAnsMap ).
thf(sk__7_type,type,
sk__7: vEntry > vQID ).
thf(sk__311_type,type,
sk__311: vQMap ).
thf('dom-Entry',axiom,
! [VX: vEntry] :
( ? [VQID0: vQID] :
( VX
= ( vask @ VQID0 ) )
| ? [VQID0: vQID,VLabel0: vLabel,VAType0: vAType] :
( VX
= ( vdefquestion @ VQID0 @ VLabel0 @ VAType0 ) )
| ? [VQID0: vQID,VAType0: vAType,VExp0: vExp] :
( VX
= ( vvalue @ VQID0 @ VAType0 @ VExp0 ) )
| ? [VQID0: vQID,VLabel0: vLabel,VAType0: vAType] :
( VX
= ( vquestion @ VQID0 @ VLabel0 @ VAType0 ) ) ) ).
thf(zip_derived_cl0,plain,
! [X0: vEntry] :
( ( X0
= ( vask @ ( sk_ @ X0 ) ) )
| ( X0
= ( vdefquestion @ ( sk__1 @ X0 ) @ ( sk__2 @ X0 ) @ ( sk__3 @ X0 ) ) )
| ( X0
= ( vvalue @ ( sk__4 @ X0 ) @ ( sk__5 @ X0 ) @ ( sk__6 @ X0 ) ) )
| ( X0
= ( vquestion @ ( sk__7 @ X0 ) @ ( sk__8 @ X0 ) @ ( sk__9 @ X0 ) ) ) ),
inference(cnf,[status(esa)],[dom-Entry]) ).
thf('Progress-qsingle',conjecture,
! [Vqm: vQMap,Vatm2: vATMap,Vqtm2: vATMap,Ve: vEntry,Vam: vAnsMap] :
( ( ~ ( visValue @ ( vqsingle @ Ve ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ Ve ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam0000: vAnsMap,Vqm0000: vQMap,Vq0000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ Ve ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam0000 @ Vqm0000 @ Vq0000 ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [Vqm: vQMap,Vatm2: vATMap,Vqtm2: vATMap,Ve: vEntry,Vam: vAnsMap] :
( ( ~ ( visValue @ ( vqsingle @ Ve ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ Ve ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam0000: vAnsMap,Vqm0000: vQMap,Vq0000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ Ve ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam0000 @ Vqm0000 @ Vq0000 ) ) ) ),
inference('cnf.neg',[status(esa)],[Progress-qsingle]) ).
thf(zip_derived_cl605,plain,
vptcheck @ ( vMC @ ( vtypeAM @ sk__315 ) @ ( vtypeQM @ sk__311 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ sk__312 @ sk__313 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf('Progress-qsingle-value',axiom,
! [Vqm: vQMap,Vt: vAType,Vatm2: vATMap,Vqtm2: vATMap,Vam: vAnsMap,Vqid: vQID,Vexp: vExp] :
( ( ~ ( visValue @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam00000: vAnsMap,Vqm00000: vQMap,Vq00000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ).
thf(zip_derived_cl601,plain,
! [X0: vExp,X1: vQID,X2: vAnsMap,X3: vAType,X4: vQMap,X5: vATMap,X6: vATMap] :
( ( ( vreduce @ ( vqsingle @ ( vvalue @ X1 @ X3 @ X0 ) ) @ X2 @ X4 )
= ( vsomeQConf @ ( vQC @ ( sk__302 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__303 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__304 @ X0 @ X1 @ X2 @ X3 @ X4 ) ) ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X2 ) @ ( vtypeQM @ X4 ) ) @ ( vqsingle @ ( vvalue @ X1 @ X3 @ X0 ) ) @ ( vMC @ X5 @ X6 ) )
| ( visValue @ ( vqsingle @ ( vvalue @ X1 @ X3 @ X0 ) ) ) ),
inference(cnf,[status(esa)],[Progress-qsingle-value]) ).
thf(zip_derived_cl606,plain,
~ ( visValue @ ( vqsingle @ sk__314 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2160,plain,
! [X0: vQMap,X1: vAnsMap,X2: vExp,X3: vAType,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vvalue @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ ( vvalue @ X4 @ X3 @ X2 ) ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ ( vvalue @ X4 @ X3 @ X2 ) ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__302 @ X2 @ X4 @ X1 @ X3 @ X0 ) @ ( sk__303 @ X2 @ X4 @ X1 @ X3 @ X0 ) @ ( sk__304 @ X2 @ X4 @ X1 @ X3 @ X0 ) ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl601,zip_derived_cl606]) ).
thf(zip_derived_cl18176,plain,
! [X0: vQMap,X1: vAnsMap,X2: vExp,X3: vAType,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vvalue @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ sk__314 ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__302 @ X2 @ X4 @ X1 @ X3 @ X0 ) @ ( sk__303 @ X2 @ X4 @ X1 @ X3 @ X0 ) @ ( sk__304 @ X2 @ X4 @ X1 @ X3 @ X0 ) ) ) ) ),
inference(local_rewriting,[status(thm)],[zip_derived_cl2160]) ).
thf(zip_derived_cl18177,plain,
! [X0: vAType,X1: vQID,X2: vExp] :
( ( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= ( vsomeQConf @ ( vQC @ ( sk__302 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) @ ( sk__303 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) @ ( sk__304 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vvalue @ X1 @ X0 @ X2 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl605,zip_derived_cl18176]) ).
thf('dom-OptQConf',axiom,
! [VX: vOptQConf] :
( ? [VQConf0: vQConf] :
( VX
= ( vsomeQConf @ VQConf0 ) )
| ( VX = vnoQConf ) ) ).
thf(zip_derived_cl50,plain,
! [X0: vOptQConf] :
( ( X0
= ( vsomeQConf @ ( sk__24 @ X0 ) ) )
| ( X0 = vnoQConf ) ),
inference(cnf,[status(esa)],[dom-OptQConf]) ).
thf('dom-QConf',axiom,
! [VX: vQConf] :
? [VAnsMap0: vAnsMap,VQMap0: vQMap,VQuestionnaire0: vQuestionnaire] :
( VX
= ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) ) ).
thf(zip_derived_cl78,plain,
! [X0: vQConf] :
( X0
= ( vQC @ ( sk__39 @ X0 ) @ ( sk__40 @ X0 ) @ ( sk__41 @ X0 ) ) ),
inference(cnf,[status(esa)],[dom-QConf]) ).
thf(zip_derived_cl604,plain,
! [X0: vAnsMap,X1: vQMap,X2: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
!= ( vsomeQConf @ ( vQC @ X0 @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl11225,plain,
! [X0: vQConf] :
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
!= ( vsomeQConf @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl78,zip_derived_cl604]) ).
thf(zip_derived_cl11226,plain,
! [X0: vOptQConf] :
( ( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
!= X0 )
| ( X0 = vnoQConf ) ),
inference('sup-',[status(thm)],[zip_derived_cl50,zip_derived_cl11225]) ).
thf(zip_derived_cl11228,plain,
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= vnoQConf ),
inference(eq_res,[status(thm)],[zip_derived_cl11226]) ).
thf(zip_derived_cl18188,plain,
! [X0: vAType,X1: vQID,X2: vExp] :
( ( vnoQConf
= ( vsomeQConf @ ( vQC @ ( sk__302 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) @ ( sk__303 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) @ ( sk__304 @ X2 @ X1 @ sk__315 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vvalue @ X1 @ X0 @ X2 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18177,zip_derived_cl11228]) ).
thf('DIFF-noQConf-someQConf',axiom,
! [VQConf0: vQConf] :
( vnoQConf
!= ( vsomeQConf @ VQConf0 ) ) ).
thf(zip_derived_cl52,plain,
! [X0: vQConf] :
( vnoQConf
!= ( vsomeQConf @ X0 ) ),
inference(cnf,[status(esa)],[DIFF-noQConf-someQConf]) ).
thf(zip_derived_cl18189,plain,
! [X0: vAType,X1: vQID,X2: vExp] :
( ( vqsingle @ ( vvalue @ X1 @ X0 @ X2 ) )
!= ( vqsingle @ sk__314 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl18188,zip_derived_cl52]) ).
thf(zip_derived_cl18191,plain,
! [X0: vEntry] :
( ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) )
| ( X0
= ( vquestion @ ( sk__7 @ X0 ) @ ( sk__8 @ X0 ) @ ( sk__9 @ X0 ) ) )
| ( X0
= ( vdefquestion @ ( sk__1 @ X0 ) @ ( sk__2 @ X0 ) @ ( sk__3 @ X0 ) ) )
| ( X0
= ( vask @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl0,zip_derived_cl18189]) ).
thf(zip_derived_cl605_001,plain,
vptcheck @ ( vMC @ ( vtypeAM @ sk__315 ) @ ( vtypeQM @ sk__311 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ sk__312 @ sk__313 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf('Progress-qsingle-defquestion',axiom,
! [Vqm: vQMap,Vt: vAType,Vatm2: vATMap,Vqtm2: vATMap,Vl: vLabel,Vam: vAnsMap,Vqid: vQID] :
( ( ~ ( visValue @ ( vqsingle @ ( vdefquestion @ Vqid @ Vl @ Vt ) ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ ( vdefquestion @ Vqid @ Vl @ Vt ) ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam00000: vAnsMap,Vqm00000: vQMap,Vq00000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ ( vdefquestion @ Vqid @ Vl @ Vt ) ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ).
thf(zip_derived_cl602,plain,
! [X0: vQID,X1: vAnsMap,X2: vLabel,X3: vAType,X4: vQMap,X5: vATMap,X6: vATMap] :
( ( ( vreduce @ ( vqsingle @ ( vdefquestion @ X0 @ X2 @ X3 ) ) @ X1 @ X4 )
= ( vsomeQConf @ ( vQC @ ( sk__305 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__306 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__307 @ X0 @ X1 @ X2 @ X3 @ X4 ) ) ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X4 ) ) @ ( vqsingle @ ( vdefquestion @ X0 @ X2 @ X3 ) ) @ ( vMC @ X5 @ X6 ) )
| ( visValue @ ( vqsingle @ ( vdefquestion @ X0 @ X2 @ X3 ) ) ) ),
inference(cnf,[status(esa)],[Progress-qsingle-defquestion]) ).
thf(zip_derived_cl606_002,plain,
~ ( visValue @ ( vqsingle @ sk__314 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2165,plain,
! [X0: vQMap,X1: vAnsMap,X2: vAType,X3: vLabel,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vdefquestion @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ ( vdefquestion @ X4 @ X3 @ X2 ) ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ ( vdefquestion @ X4 @ X3 @ X2 ) ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__305 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__306 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__307 @ X4 @ X1 @ X3 @ X2 @ X0 ) ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl602,zip_derived_cl606]) ).
thf(zip_derived_cl18390,plain,
! [X0: vQMap,X1: vAnsMap,X2: vAType,X3: vLabel,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vdefquestion @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ sk__314 ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__305 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__306 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__307 @ X4 @ X1 @ X3 @ X2 @ X0 ) ) ) ) ),
inference(local_rewriting,[status(thm)],[zip_derived_cl2165]) ).
thf(zip_derived_cl18391,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= ( vsomeQConf @ ( vQC @ ( sk__305 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__306 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__307 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vdefquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl605,zip_derived_cl18390]) ).
thf(zip_derived_cl11228_003,plain,
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= vnoQConf ),
inference(eq_res,[status(thm)],[zip_derived_cl11226]) ).
thf(zip_derived_cl18402,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( vnoQConf
= ( vsomeQConf @ ( vQC @ ( sk__305 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__306 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__307 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vdefquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18391,zip_derived_cl11228]) ).
thf(zip_derived_cl52_004,plain,
! [X0: vQConf] :
( vnoQConf
!= ( vsomeQConf @ X0 ) ),
inference(cnf,[status(esa)],[DIFF-noQConf-someQConf]) ).
thf(zip_derived_cl18403,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( vqsingle @ ( vdefquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl18402,zip_derived_cl52]) ).
thf(zip_derived_cl18438,plain,
! [X0: vEntry] :
( ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) )
| ( X0
= ( vask @ ( sk_ @ X0 ) ) )
| ( X0
= ( vquestion @ ( sk__7 @ X0 ) @ ( sk__8 @ X0 ) @ ( sk__9 @ X0 ) ) )
| ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl18191,zip_derived_cl18403]) ).
thf(zip_derived_cl18439,plain,
! [X0: vEntry] :
( ( X0
= ( vquestion @ ( sk__7 @ X0 ) @ ( sk__8 @ X0 ) @ ( sk__9 @ X0 ) ) )
| ( X0
= ( vask @ ( sk_ @ X0 ) ) )
| ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl18438]) ).
thf(zip_derived_cl605_005,plain,
vptcheck @ ( vMC @ ( vtypeAM @ sk__315 ) @ ( vtypeQM @ sk__311 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ sk__312 @ sk__313 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf('Progress-qsingle-question',axiom,
! [Vqm: vQMap,Vt: vAType,Vatm2: vATMap,Vqtm2: vATMap,Vl: vLabel,Vam: vAnsMap,Vqid: vQID] :
( ( ~ ( visValue @ ( vqsingle @ ( vquestion @ Vqid @ Vl @ Vt ) ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ ( vquestion @ Vqid @ Vl @ Vt ) ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam00000: vAnsMap,Vqm00000: vQMap,Vq00000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ ( vquestion @ Vqid @ Vl @ Vt ) ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ).
thf(zip_derived_cl600,plain,
! [X0: vQID,X1: vAnsMap,X2: vLabel,X3: vAType,X4: vQMap,X5: vATMap,X6: vATMap] :
( ( ( vreduce @ ( vqsingle @ ( vquestion @ X0 @ X2 @ X3 ) ) @ X1 @ X4 )
= ( vsomeQConf @ ( vQC @ ( sk__299 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__300 @ X0 @ X1 @ X2 @ X3 @ X4 ) @ ( sk__301 @ X0 @ X1 @ X2 @ X3 @ X4 ) ) ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X4 ) ) @ ( vqsingle @ ( vquestion @ X0 @ X2 @ X3 ) ) @ ( vMC @ X5 @ X6 ) )
| ( visValue @ ( vqsingle @ ( vquestion @ X0 @ X2 @ X3 ) ) ) ),
inference(cnf,[status(esa)],[Progress-qsingle-question]) ).
thf(zip_derived_cl606_006,plain,
~ ( visValue @ ( vqsingle @ sk__314 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2155,plain,
! [X0: vQMap,X1: vAnsMap,X2: vAType,X3: vLabel,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vquestion @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ ( vquestion @ X4 @ X3 @ X2 ) ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ ( vquestion @ X4 @ X3 @ X2 ) ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__299 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__300 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__301 @ X4 @ X1 @ X3 @ X2 @ X0 ) ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl600,zip_derived_cl606]) ).
thf(zip_derived_cl18105,plain,
! [X0: vQMap,X1: vAnsMap,X2: vAType,X3: vLabel,X4: vQID,X5: vATMap,X6: vATMap] :
( ( ( vqsingle @ ( vquestion @ X4 @ X3 @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ X6 @ X5 ) )
| ( ( vreduce @ ( vqsingle @ sk__314 ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__299 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__300 @ X4 @ X1 @ X3 @ X2 @ X0 ) @ ( sk__301 @ X4 @ X1 @ X3 @ X2 @ X0 ) ) ) ) ),
inference(local_rewriting,[status(thm)],[zip_derived_cl2155]) ).
thf(zip_derived_cl18106,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= ( vsomeQConf @ ( vQC @ ( sk__299 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__300 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__301 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl605,zip_derived_cl18105]) ).
thf(zip_derived_cl11228_007,plain,
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= vnoQConf ),
inference(eq_res,[status(thm)],[zip_derived_cl11226]) ).
thf(zip_derived_cl18117,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( vnoQConf
= ( vsomeQConf @ ( vQC @ ( sk__299 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__300 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) @ ( sk__301 @ X2 @ sk__315 @ X1 @ X0 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18106,zip_derived_cl11228]) ).
thf(zip_derived_cl52_008,plain,
! [X0: vQConf] :
( vnoQConf
!= ( vsomeQConf @ X0 ) ),
inference(cnf,[status(esa)],[DIFF-noQConf-someQConf]) ).
thf(zip_derived_cl18118,plain,
! [X0: vAType,X1: vLabel,X2: vQID] :
( ( vqsingle @ ( vquestion @ X2 @ X1 @ X0 ) )
!= ( vqsingle @ sk__314 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl18117,zip_derived_cl52]) ).
thf(zip_derived_cl18749,plain,
! [X0: vEntry] :
( ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) )
| ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) )
| ( X0
= ( vask @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl18439,zip_derived_cl18118]) ).
thf(zip_derived_cl18750,plain,
! [X0: vEntry] :
( ( X0
= ( vask @ ( sk_ @ X0 ) ) )
| ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl18749]) ).
thf(zip_derived_cl605_009,plain,
vptcheck @ ( vMC @ ( vtypeAM @ sk__315 ) @ ( vtypeQM @ sk__311 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ sk__312 @ sk__313 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf('Progress-qsingle-ask',axiom,
! [Vqm: vQMap,Vatm2: vATMap,Vqtm2: vATMap,Vam: vAnsMap,Vqid: vQID] :
( ( ~ ( visValue @ ( vqsingle @ ( vask @ Vqid ) ) )
& ( vptcheck @ ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @ ( vqsingle @ ( vask @ Vqid ) ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) )
=> ? [Vam00000: vAnsMap,Vqm00000: vQMap,Vq00000: vQuestionnaire] :
( ( vreduce @ ( vqsingle @ ( vask @ Vqid ) ) @ Vam @ Vqm )
= ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ).
thf(zip_derived_cl603,plain,
! [X0: vQID,X1: vAnsMap,X2: vQMap,X3: vATMap,X4: vATMap] :
( ( ( vreduce @ ( vqsingle @ ( vask @ X0 ) ) @ X1 @ X2 )
= ( vsomeQConf @ ( vQC @ ( sk__308 @ X0 @ X1 @ X2 ) @ ( sk__309 @ X0 @ X1 @ X2 ) @ ( sk__310 @ X0 @ X1 @ X2 ) ) ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X2 ) ) @ ( vqsingle @ ( vask @ X0 ) ) @ ( vMC @ X3 @ X4 ) )
| ( visValue @ ( vqsingle @ ( vask @ X0 ) ) ) ),
inference(cnf,[status(esa)],[Progress-qsingle-ask]) ).
thf(zip_derived_cl606_010,plain,
~ ( visValue @ ( vqsingle @ sk__314 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2170,plain,
! [X0: vQMap,X1: vAnsMap,X2: vQID,X3: vATMap,X4: vATMap] :
( ( ( vqsingle @ ( vask @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ ( vask @ X2 ) ) @ ( vMC @ X4 @ X3 ) )
| ( ( vreduce @ ( vqsingle @ ( vask @ X2 ) ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__308 @ X2 @ X1 @ X0 ) @ ( sk__309 @ X2 @ X1 @ X0 ) @ ( sk__310 @ X2 @ X1 @ X0 ) ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl603,zip_derived_cl606]) ).
thf(zip_derived_cl18558,plain,
! [X0: vQMap,X1: vAnsMap,X2: vQID,X3: vATMap,X4: vATMap] :
( ( ( vqsingle @ ( vask @ X2 ) )
!= ( vqsingle @ sk__314 ) )
| ~ ( vptcheck @ ( vMC @ ( vtypeAM @ X1 ) @ ( vtypeQM @ X0 ) ) @ ( vqsingle @ sk__314 ) @ ( vMC @ X4 @ X3 ) )
| ( ( vreduce @ ( vqsingle @ sk__314 ) @ X1 @ X0 )
= ( vsomeQConf @ ( vQC @ ( sk__308 @ X2 @ X1 @ X0 ) @ ( sk__309 @ X2 @ X1 @ X0 ) @ ( sk__310 @ X2 @ X1 @ X0 ) ) ) ) ),
inference(local_rewriting,[status(thm)],[zip_derived_cl2170]) ).
thf(zip_derived_cl18559,plain,
! [X0: vQID] :
( ( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= ( vsomeQConf @ ( vQC @ ( sk__308 @ X0 @ sk__315 @ sk__311 ) @ ( sk__309 @ X0 @ sk__315 @ sk__311 ) @ ( sk__310 @ X0 @ sk__315 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vask @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl605,zip_derived_cl18558]) ).
thf(zip_derived_cl11228_011,plain,
( ( vreduce @ ( vqsingle @ sk__314 ) @ sk__315 @ sk__311 )
= vnoQConf ),
inference(eq_res,[status(thm)],[zip_derived_cl11226]) ).
thf(zip_derived_cl18570,plain,
! [X0: vQID] :
( ( vnoQConf
= ( vsomeQConf @ ( vQC @ ( sk__308 @ X0 @ sk__315 @ sk__311 ) @ ( sk__309 @ X0 @ sk__315 @ sk__311 ) @ ( sk__310 @ X0 @ sk__315 @ sk__311 ) ) ) )
| ( ( vqsingle @ ( vask @ X0 ) )
!= ( vqsingle @ sk__314 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18559,zip_derived_cl11228]) ).
thf(zip_derived_cl52_012,plain,
! [X0: vQConf] :
( vnoQConf
!= ( vsomeQConf @ X0 ) ),
inference(cnf,[status(esa)],[DIFF-noQConf-someQConf]) ).
thf(zip_derived_cl18571,plain,
! [X0: vQID] :
( ( vqsingle @ ( vask @ X0 ) )
!= ( vqsingle @ sk__314 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl18570,zip_derived_cl52]) ).
thf(zip_derived_cl18758,plain,
! [X0: vEntry] :
( ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) )
| ( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl18750,zip_derived_cl18571]) ).
thf(zip_derived_cl18776,plain,
! [X0: vEntry] :
( ( vqsingle @ X0 )
!= ( vqsingle @ sk__314 ) ),
inference(simplify,[status(thm)],[zip_derived_cl18758]) ).
thf(zip_derived_cl18777,plain,
$false,
inference(eq_res,[status(thm)],[zip_derived_cl18776]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : COM266_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.TvcA7DhBr4 true
% 0.18/0.35 % Computer : n018.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Mon May 4 20:00:02 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 % Running portfolio for 300 s
% 0.18/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.35 % Number of cores: 8
% 0.18/0.35 % Python version: Python 3.6.8
% 0.18/0.36 % Running in FO mode
% 0.55/0.65 % Total configuration time : 435
% 0.55/0.65 % Estimated wc time : 1092
% 0.55/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 33.07/5.37 % Solved by fo/fo3_bce.sh.
% 33.07/5.37 % BCE start: 607
% 33.07/5.37 % BCE eliminated: 0
% 33.07/5.37 % PE start: 607
% 33.07/5.37 logic: eq
% 33.07/5.37 % PE eliminated: -327
% 33.07/5.37 % done 1982 iterations in 4.622s
% 33.07/5.37 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 33.07/5.37 % SZS output start Refutation
% See solution above
% 33.07/5.37
% 33.07/5.37
% 33.07/5.37 % Terminating...
% 33.79/5.46 % Runner terminated.
% 33.79/5.47 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------