Anne is big. Anne is cold. Anne is smart. Charlie is big. Charlie is blue. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is smart. Dave is big. Dave is cold. Dave is red. If someone is kind then they are quiet. Blue, red people are big. If Charlie is quiet and Charlie is red then Charlie is blue. If Dave is smart and Dave is quiet then Dave is big. All cold people are quiet. If someone is smart then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Blue, red people are big.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Charlie is quiet and Charlie is red then Charlie is blue.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "+"))
If Dave is smart and Dave is quiet then Dave is big.
((("Dave" "is" "smart" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "big" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3) -> rule6))]
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is not quiet.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule1))]
("Charlie" "is" "quiet" "-")
triple7
((triple6) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule6))] Anne is cold.[(triple2)] Anne is smart.[(triple3)] Charlie is big.[(triple4 OR ((triple9) -> rule6) OR ((triple5 triple8) -> rule2) OR ((((triple7 triple8) -> rule3) triple8) -> rule2) OR ((((((triple6) -> rule1) triple8) -> rule3) triple8) -> rule2))] Charlie is blue.[(triple5 OR ((triple7 triple8) -> rule3) OR ((((triple6) -> rule1) triple8) -> rule3))] Charlie is kind.[(triple6)] Charlie is quiet.[(triple7 OR ((triple6) -> rule1))] Charlie is red.[(triple8)] Charlie is smart.[(triple9)] Dave is big.[(triple10)] Dave is cold.[(triple11)] Dave is red.[(triple12)] @1: Anne is quiet.[(((triple2) -> rule5))] Dave is quiet.[(((triple11) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple9) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 triple8) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7 triple8) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple6) -> (rule1 % int3)) triple8) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple7 triple8) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple6) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((triple6) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple11) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1