Anne is blue. Anne is cold. Anne is green. Anne is smart. Anne is white. Dave is blue. Dave is green. Dave is quiet. Dave is smart. Dave is white. Erin is big. Erin is blue. Erin is cold. Erin is quiet. Erin is smart. Smart things are quiet. Green, quiet things are big. All big things are blue. If Anne is quiet and Anne is blue then Anne is smart. If something is smart and blue then it is green. If Anne is smart then Anne is green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Green, quiet things are big.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Anne is quiet and Anne is blue then Anne is smart.
((("Anne" "is" "quiet" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "smart" "+"))
If something is smart and blue then it is green.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Anne is smart then Anne is green.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "green" "+"))
Dave is smart.
True
1
proof
[(triple9)]
("Dave" "is" "smart" "+")
triple9
Dave is not green.
False
1
inv-proof
[(triple7 OR ((triple9 triple6) -> rule5))]
("Dave" "is" "green" "-")
triple7
((triple9 triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is green.
True
3
proof
[(((triple15 triple12) -> rule5) OR ((triple15 ((triple11) -> rule3)) -> rule5))]
("Erin" "is" "green" "+")
((triple15 triple12) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple15 ((triple11) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Anne is not quiet.
False
2
inv-proof
[(((triple4) -> rule1))]
("Anne" "is" "quiet" "-")
((triple4) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
True
4
proof
[(((triple3 ((triple4) -> rule1)) -> rule2) OR ((((triple4) -> rule6) ((triple4) -> rule1)) -> rule2) OR ((((triple4 triple1) -> rule5) ((triple4) -> rule1)) -> rule2))]
("Anne" "is" "big" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4 triple1) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not big.
False
4
inv-proof
[(((triple3 ((triple4) -> rule1)) -> rule2) OR ((((triple4) -> rule6) ((triple4) -> rule1)) -> rule2) OR ((((triple4 triple1) -> rule5) ((triple4) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4 triple1) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is blue.[(triple1 OR ((((triple3 ((triple4) -> rule1)) -> rule2)) -> rule3) OR ((((((triple4) -> rule6) ((triple4) -> rule1)) -> rule2)) -> rule3))] Anne is cold.[(triple2)] Anne is green.[(triple3 OR ((triple4) -> rule6) OR ((triple4 triple1) -> rule5))] Anne is smart.[(triple4)] Anne is white.[(triple5)] Dave is blue.[(triple6 OR ((((triple7 triple8) -> rule2)) -> rule3) OR ((((triple7 ((triple9) -> rule1)) -> rule2)) -> rule3))] Dave is green.[(triple7 OR ((triple9 triple6) -> rule5))] Dave is quiet.[(triple8 OR ((triple9) -> rule1))] Dave is smart.[(triple9)] Dave is white.[(triple10)] Erin is big.[(triple11 OR ((((triple15 triple12) -> rule5) triple14) -> rule2) OR ((((triple15 triple12) -> rule5) ((triple15) -> rule1)) -> rule2))] Erin is blue.[(triple12 OR ((triple11) -> rule3))] Erin is cold.[(triple13)] Erin is quiet.[(triple14 OR ((triple15) -> rule1))] Erin is smart.[(triple15)] @1: Anne is quiet.[(((triple4) -> rule1))] Dave is big.[(((triple7 triple8) -> rule2) OR ((triple7 ((triple9) -> rule1)) -> rule2) OR ((((triple9 triple6) -> rule5) triple8) -> rule2) OR ((((triple9 triple6) -> rule5) ((triple9) -> rule1)) -> rule2))] Erin is green.[(((triple15 triple12) -> rule5) OR ((triple15 ((triple11) -> rule3)) -> rule5))] @2: Anne is big.[(((triple3 ((triple4) -> rule1)) -> rule2) OR ((((triple4) -> rule6) ((triple4) -> rule1)) -> rule2) OR ((((triple4 triple1) -> rule5) ((triple4) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple3 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((triple4) -> (rule6 % int4)) ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((((triple7 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple7 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple9 triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple9) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((((triple15 triple12) -> (rule5 % int2)) triple14) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple15 triple12) -> (rule5 % int3)) ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple12
((triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple13
Erin is quiet.
("Erin" "is" "quiet" "+")
triple14
((triple15) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple7 triple8) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple7 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple9 triple6) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple9 triple6) -> (rule5 % int3)) ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple15 triple12) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple15 ((triple11) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple4 triple1) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3