%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM269_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.p9dpDfMhqV true
% Computer : n028.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 21.68s 3.73s
% Output : Refutation 21.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : COM269_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.p9dpDfMhqV true
% 0.17/0.36 % Computer : n028.cluster.edu
% 0.17/0.36 % Model : x86_64 x86_64
% 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.36 % Memory : 8042.1875MB
% 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.36 % CPULimit : 300
% 0.17/0.36 % WCLimit : 300
% 0.17/0.36 % DateTime : Mon May 4 20:02:45 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 % Running portfolio for 300 s
% 0.17/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.36 % Number of cores: 8
% 0.17/0.37 % Python version: Python 3.6.8
% 0.17/0.37 % Running in FO mode
% 0.53/0.69 % Total configuration time : 435
% 0.53/0.69 % Estimated wc time : 1092
% 0.53/0.69 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.78 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 21.68/3.73 % Solved by fo/fo3_bce.sh.
% 21.68/3.73 % BCE start: 760
% 21.68/3.73 % BCE eliminated: 0
% 21.68/3.73 % PE start: 760
% 21.68/3.73 logic: eq
% 21.68/3.73 % PE eliminated: -355
% 21.68/3.73 % done 929 iterations in 2.957s
% 21.68/3.73 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 21.68/3.73 % SZS output start Refutation
% 21.68/3.73 thf(vOptQConf_type, type, vOptQConf: $tType).
% 21.68/3.73 thf(vQConf_type, type, vQConf: $tType).
% 21.68/3.73 thf(vAnsMap_type, type, vAnsMap: $tType).
% 21.68/3.73 thf(vQMap_type, type, vQMap: $tType).
% 21.68/3.73 thf(vQuestionnaire_type, type, vQuestionnaire: $tType).
% 21.68/3.73 thf(vOptExp_type, type, vOptExp: $tType).
% 21.68/3.73 thf(vExp_type, type, vExp: $tType).
% 21.68/3.73 thf(vEntry_type, type, vEntry: $tType).
% 21.68/3.73 thf(vQID_type, type, vQID: $tType).
% 21.68/3.73 thf(vAType_type, type, vAType: $tType).
% 21.68/3.73 thf(vMapConf_type, type, vMapConf: $tType).
% 21.68/3.73 thf(vATMap_type, type, vATMap: $tType).
% 21.68/3.73 thf(vgetExp_type, type, vgetExp: vOptExp > vExp).
% 21.68/3.73 thf(vsomeQConf_type, type, vsomeQConf: vQConf > vOptQConf).
% 21.68/3.73 thf(vnoQConf_type, type, vnoQConf: vOptQConf).
% 21.68/3.73 thf(sk__48_type, type, sk__48: vQConf > vQMap).
% 21.68/3.73 thf(sk__341_type, type, sk__341: vAType).
% 21.68/3.73 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 21.68/3.73 thf(vreduce_type, type, vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf).
% 21.68/3.73 thf(sk__344_type, type, sk__344: vAnsMap).
% 21.68/3.73 thf(vtypeQM_type, type, vtypeQM: vQMap > vATMap).
% 21.68/3.73 thf(sk__340_type, type, sk__340: vQMap).
% 21.68/3.73 thf(vptcheck_type, type, vptcheck: vMapConf > vQuestionnaire > vMapConf > $o).
% 21.68/3.73 thf(sk__47_type, type, sk__47: vQConf > vAnsMap).
% 21.68/3.73 thf(vMC_type, type, vMC: vATMap > vATMap > vMapConf).
% 21.68/3.73 thf(vqsingle_type, type, vqsingle: vEntry > vQuestionnaire).
% 21.68/3.73 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 21.68/3.73 thf(visSomeExp_type, type, visSomeExp: vOptExp > $o).
% 21.68/3.73 thf(visValue_type, type, visValue: vQuestionnaire > $o).
% 21.68/3.73 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 21.68/3.73 thf(sk__49_type, type, sk__49: vQConf > vQuestionnaire).
% 21.68/3.73 thf(vQC_type, type, vQC: vAnsMap > vQMap > vQuestionnaire > vQConf).
% 21.68/3.73 thf(sk__345_type, type, sk__345: vQID).
% 21.68/3.73 thf(sk__32_type, type, sk__32: vOptQConf > vQConf).
% 21.68/3.73 thf(vvalue_type, type, vvalue: vQID > vAType > vExp > vEntry).
% 21.68/3.73 thf(sk__346_type, type, sk__346: vExp).
% 21.68/3.73 thf('dom-OptQConf', axiom,
% 21.68/3.73 (![VX:vOptQConf]:
% 21.68/3.73 ( ( ?[VQConf0:vQConf]: ( ( VX ) = ( vsomeQConf @ VQConf0 ) ) ) |
% 21.68/3.73 ( ( VX ) = ( vnoQConf ) ) ))).
% 21.68/3.73 thf(zip_derived_cl67, plain,
% 21.68/3.73 (![X0 : vOptQConf]:
% 21.68/3.73 (((X0) = (vsomeQConf @ (sk__32 @ X0))) | ((X0) = (vnoQConf)))),
% 21.68/3.73 inference('cnf', [status(esa)], [dom-OptQConf])).
% 21.68/3.73 thf('dom-QConf', axiom,
% 21.68/3.73 (![VX:vQConf]:
% 21.68/3.73 ( ?[VAnsMap0:vAnsMap,VQMap0:vQMap,VQuestionnaire0:vQuestionnaire]:
% 21.68/3.73 ( ( VX ) = ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) ) ))).
% 21.68/3.73 thf(zip_derived_cl135, plain,
% 21.68/3.73 (![X0 : vQConf]:
% 21.68/3.73 ((X0) = (vQC @ (sk__47 @ X0) @ (sk__48 @ X0) @ (sk__49 @ X0)))),
% 21.68/3.73 inference('cnf', [status(esa)], [dom-QConf])).
% 21.68/3.73 thf('Progress-qsingle-value-expIsValue-False-isSomeExp-True', conjecture,
% 21.68/3.73 (![Vqm:vQMap,Vt:vAType,Vatm2:vATMap,Vqtm2:vATMap,Vam:vAnsMap,Vqid:vQID,
% 21.68/3.73 Vexp:vExp]:
% 21.68/3.73 ( ( ( visSomeExp @ ( vreduceExp @ Vexp @ Vam ) ) &
% 21.68/3.73 ( ~( vexpIsValue @ Vexp ) ) &
% 21.68/3.73 ( ~( visValue @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) ) ) &
% 21.68/3.73 ( vptcheck @
% 21.68/3.73 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 21.68/3.73 ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @
% 21.68/3.73 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 21.68/3.73 ( ?[Vam000000:vAnsMap,Vqm000000:vQMap,Vq000000:vQuestionnaire]:
% 21.68/3.73 ( ( vreduce @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @ Vam @ Vqm ) =
% 21.68/3.73 ( vsomeQConf @ ( vQC @ Vam000000 @ Vqm000000 @ Vq000000 ) ) ) ) ))).
% 21.68/3.73 thf(zf_stmt_0, negated_conjecture,
% 21.68/3.73 (~( ![Vqm:vQMap,Vt:vAType,Vatm2:vATMap,Vqtm2:vATMap,Vam:vAnsMap,Vqid:vQID,
% 21.68/3.73 Vexp:vExp]:
% 21.68/3.73 ( ( ( visSomeExp @ ( vreduceExp @ Vexp @ Vam ) ) &
% 21.68/3.73 ( ~( vexpIsValue @ Vexp ) ) &
% 21.68/3.73 ( ~( visValue @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) ) ) &
% 21.68/3.73 ( vptcheck @
% 21.68/3.73 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 21.68/3.73 ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @
% 21.68/3.73 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 21.68/3.73 ( ?[Vam000000:vAnsMap,Vqm000000:vQMap,Vq000000:vQuestionnaire]:
% 21.68/3.73 ( ( vreduce @
% 21.68/3.73 ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @ Vam @ Vqm ) =
% 21.68/3.73 ( vsomeQConf @ ( vQC @ Vam000000 @ Vqm000000 @ Vq000000 ) ) ) ) ) )),
% 21.68/3.73 inference('cnf.neg', [status(esa)],
% 21.68/3.73 [Progress-qsingle-value-expIsValue-False-isSomeExp-True])).
% 21.68/3.73 thf(zip_derived_cl759, plain,
% 21.68/3.73 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire]:
% 21.68/3.73 ((vreduce @ (vqsingle @ (vvalue @ sk__345 @ sk__341 @ sk__346)) @
% 21.68/3.73 sk__344 @ sk__340) != (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 21.68/3.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.68/3.73 thf(zip_derived_cl11638, plain,
% 21.68/3.73 (![X0 : vQConf]:
% 21.68/3.73 ((vreduce @ (vqsingle @ (vvalue @ sk__345 @ sk__341 @ sk__346)) @
% 21.68/3.73 sk__344 @ sk__340) != (vsomeQConf @ X0))),
% 21.68/3.73 inference('sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl759])).
% 21.68/3.73 thf(zip_derived_cl11643, plain,
% 21.68/3.73 (![X0 : vOptQConf]:
% 21.68/3.73 (((vreduce @ (vqsingle @ (vvalue @ sk__345 @ sk__341 @ sk__346)) @
% 21.68/3.73 sk__344 @ sk__340) != (X0))
% 21.68/3.73 | ((X0) = (vnoQConf)))),
% 21.68/3.73 inference('sup-', [status(thm)], [zip_derived_cl67, zip_derived_cl11638])).
% 21.68/3.73 thf(zip_derived_cl11667, plain,
% 21.68/3.73 (((vreduce @ (vqsingle @ (vvalue @ sk__345 @ sk__341 @ sk__346)) @
% 21.68/3.73 sk__344 @ sk__340) = (vnoQConf))),
% 21.68/3.73 inference('eq_res', [status(thm)], [zip_derived_cl11643])).
% 21.68/3.73 thf('reduce-3', axiom,
% 21.68/3.73 (![Vqm:vQMap,Vt:vAType,Vam:vAnsMap,Vqid:vQID,Vexp:vExp]:
% 21.68/3.73 ( ( ( ~( vexpIsValue @ Vexp ) ) &
% 21.68/3.73 ( visSomeExp @ ( vreduceExp @ Vexp @ Vam ) ) ) =>
% 21.68/3.73 ( ( vreduce @ ( vqsingle @ ( vvalue @ Vqid @ Vt @ Vexp ) ) @ Vam @ Vqm ) =
% 21.68/3.73 ( vsomeQConf @
% 21.68/3.73 ( vQC @
% 21.68/3.73 Vam @ Vqm @
% 21.68/3.73 ( vqsingle @
% 21.68/3.73 ( vvalue @ Vqid @ Vt @ ( vgetExp @ ( vreduceExp @ Vexp @ Vam ) ) ) ) ) ) ) ))).
% 21.68/3.73 thf(zip_derived_cl423, plain,
% 21.68/3.73 (![X0 : vAnsMap, X1 : vQMap, X2 : vQID, X3 : vAType, X4 : vExp]:
% 21.68/3.73 (((vreduce @ (vqsingle @ (vvalue @ X2 @ X3 @ X4)) @ X0 @ X1)
% 21.68/3.73 = (vsomeQConf @
% 21.68/3.73 (vQC @ X0 @ X1 @
% 21.68/3.73 (vqsingle @
% 21.68/3.73 (vvalue @ X2 @ X3 @ (vgetExp @ (vreduceExp @ X4 @ X0)))))))
% 21.68/3.73 | ~ (visSomeExp @ (vreduceExp @ X4 @ X0))
% 21.68/3.73 | (vexpIsValue @ X4))),
% 21.68/3.73 inference('cnf', [status(esa)], [reduce-3])).
% 21.68/3.73 thf(zip_derived_cl12613, plain,
% 21.68/3.73 ((((vnoQConf)
% 21.68/3.73 = (vsomeQConf @
% 21.68/3.73 (vQC @ sk__344 @ sk__340 @
% 21.68/3.73 (vqsingle @
% 21.68/3.73 (vvalue @ sk__345 @ sk__341 @
% 21.68/3.73 (vgetExp @ (vreduceExp @ sk__346 @ sk__344)))))))
% 21.68/3.73 | (vexpIsValue @ sk__346)
% 21.68/3.73 | ~ (visSomeExp @ (vreduceExp @ sk__346 @ sk__344)))),
% 21.68/3.73 inference('sup+', [status(thm)], [zip_derived_cl11667, zip_derived_cl423])).
% 21.68/3.73 thf(zip_derived_cl756, plain, (~ (vexpIsValue @ sk__346)),
% 21.68/3.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.68/3.73 thf(zip_derived_cl755, plain,
% 21.68/3.73 ( (visSomeExp @ (vreduceExp @ sk__346 @ sk__344))),
% 21.68/3.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.68/3.73 thf(zip_derived_cl12615, plain,
% 21.68/3.73 (((vnoQConf)
% 21.68/3.73 = (vsomeQConf @
% 21.68/3.73 (vQC @ sk__344 @ sk__340 @
% 21.68/3.73 (vqsingle @
% 21.68/3.73 (vvalue @ sk__345 @ sk__341 @
% 21.68/3.73 (vgetExp @ (vreduceExp @ sk__346 @ sk__344)))))))),
% 21.68/3.73 inference('demod', [status(thm)],
% 21.68/3.73 [zip_derived_cl12613, zip_derived_cl756, zip_derived_cl755])).
% 21.68/3.73 thf('DIFF-noQConf-someQConf', axiom,
% 21.68/3.73 (![VQConf0:vQConf]: ( ( vnoQConf ) != ( vsomeQConf @ VQConf0 ) ))).
% 21.68/3.73 thf(zip_derived_cl69, plain,
% 21.68/3.73 (![X0 : vQConf]: ((vnoQConf) != (vsomeQConf @ X0))),
% 21.68/3.73 inference('cnf', [status(esa)], [DIFF-noQConf-someQConf])).
% 21.68/3.73 thf(zip_derived_cl12616, plain, ($false),
% 21.68/3.73 inference('simplify_reflect-', [status(thm)],
% 21.68/3.73 [zip_derived_cl12615, zip_derived_cl69])).
% 21.68/3.73
% 21.68/3.73 % SZS output end Refutation
% 21.68/3.73
% 21.68/3.73
% 21.68/3.73 % Terminating...
% 4.41/3.80 % Runner terminated.
% 4.41/3.80 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------