Anne is quiet. Bob is quiet. Bob is red. Dave is not cold. Dave is young. Erin is round. Erin is young. All young people are quiet. If Bob is rough then Bob is not round. Round, quiet people are red. All red people are round. Young people are round. All red, young people are not cold. If Anne is quiet then Anne is big. If Anne is big then Anne is young. If Bob is round and Bob is red then Bob is not young.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is rough then Bob is not round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "-"))
Round, quiet people are red.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All red, young people are not cold.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "-"))
If Anne is quiet then Anne is big.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "big" "+"))
If Anne is big then Anne is young.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "young" "+"))
If Bob is round and Bob is red then Bob is not young.
((("Bob" "is" "round" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "young" "-"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple7)]
("Erin" "is" "young" "-")
triple7
Dave is quiet.
True
2
proof
[(((triple5) -> rule1))]
("Dave" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple5) -> rule1))]
("Dave" "is" "quiet" "-")
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule7)) -> rule8))]
("Anne" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8))]
("Anne" "is" "young" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
True
4
proof
[(((((((triple1) -> rule7)) -> rule8)) -> rule5))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule8)) -> rule5))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is red.
True
6
proof
[(((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3))]
("Anne" "is" "red" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not red.
False
6
inv-proof
[(((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3))]
("Anne" "is" "red" "-")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not cold.
True
10
proof
[(((((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3) ((((triple1) -> rule7)) -> rule8)) -> rule6))]
("Anne" "is" "cold" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple1) -> (rule3 % int2)) ((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is cold.
False
10
inv-proof
[(((((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3) ((((triple1) -> rule7)) -> rule8)) -> rule6))]
("Anne" "is" "cold" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple1) -> (rule3 % int2)) ((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is quiet.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Dave is not cold.[(triple4 OR ((((((triple5) -> rule5) ((triple5) -> rule1)) -> rule3) triple5) -> rule6))] Dave is young.[(triple5)] Erin is round.[(triple6 OR ((triple7) -> rule5))] Erin is young.[(triple7)] @1: Anne is big.[(((triple1) -> rule7))] Bob is round.[(((triple3) -> rule4))] Dave is quiet.[(((triple5) -> rule1))] Dave is round.[(((triple5) -> rule5))] Erin is quiet.[(((triple7) -> rule1))] @2: Anne is young.[(((((triple1) -> rule7)) -> rule8))] Bob is not young.[(((((triple3) -> rule4) triple3) -> rule9))] Dave is red.[(((((triple5) -> rule5) ((triple5) -> rule1)) -> rule3))] Erin is red.[(((triple6 ((triple7) -> rule1)) -> rule3) OR ((((triple7) -> rule5) ((triple7) -> rule1)) -> rule3))] @3: Anne is round.[(((((((triple1) -> rule7)) -> rule8)) -> rule5))] Erin is not cold.[(((((triple6 ((triple7) -> rule1)) -> rule3) triple7) -> rule6) OR ((((((triple7) -> rule5) ((triple7) -> rule1)) -> rule3) triple7) -> rule6))] @4: Anne is red.[(((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3))] @5: Anne is not cold.[(((((((((((triple1) -> rule7)) -> rule8)) -> rule5) triple1) -> rule3) ((((triple1) -> rule7)) -> rule8)) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Dave is not cold.
("Dave" "is" "cold" "-")
triple4
((((((triple5) -> (rule5 % int4)) ((triple5) -> (rule1 % int3))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple7) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is not young.
("Bob" "is" "young" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule9 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple5) -> (rule5 % int3)) ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple6 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple7) -> (rule5 % int4)) ((triple7) -> (rule1 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not cold.
("Anne" "is" "cold" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple1) -> (rule3 % int2)) ((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5