Anne is big. Anne is green. Anne is quiet. Anne is round. Bob is kind. Bob is quiet. Bob is red. Bob is white. Charlie is red. Charlie is round. Quiet people are white. If someone is round then they are quiet. If someone is red and green then they are round. All red, white people are round. All quiet people are round. If someone is red and white then they are quiet. All quiet people are big. If Bob is big and Bob is round then Bob is quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red and green then they are round.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All red, white people are round.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is red and white then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Bob is big and Bob is round then Bob is quiet.
((("Bob" "is" "big" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple6 OR ((triple7 triple8) -> rule6) OR ((((triple7 triple8) -> rule4)) -> rule2))]
("Bob" "is" "quiet" "+")
triple6
((triple7 triple8) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7 triple8) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Anne is not quiet.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule2))]
("Anne" "is" "quiet" "-")
triple3
((triple4) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is big.
True
2
proof
[(((triple6) -> rule7) OR ((((triple7 triple8) -> rule6)) -> rule7) OR ((((((triple7 triple8) -> rule4)) -> rule2)) -> rule7))]
("Bob" "is" "big" "+")
((triple6) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7 triple8) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple7 triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Anne is not white.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is big.
True
3
proof
[(((((triple10) -> rule2)) -> rule7))]
("Charlie" "is" "big" "+")
((((triple10) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule7) OR ((((triple4) -> rule2)) -> rule7))] Anne is green.[(triple2)] Anne is quiet.[(triple3 OR ((triple4) -> rule2))] Anne is round.[(triple4 OR ((triple3) -> rule5))] Bob is kind.[(triple5)] Bob is quiet.[(triple6 OR ((triple7 triple8) -> rule6) OR ((((triple7 triple8) -> rule4)) -> rule2))] Bob is red.[(triple7)] Bob is white.[(triple8 OR ((triple6) -> rule1))] Charlie is red.[(triple9)] Charlie is round.[(triple10)] @1: Anne is white.[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))] Bob is big.[(((triple6) -> rule7) OR ((((triple7 triple8) -> rule6)) -> rule7) OR ((((((triple7 triple8) -> rule4)) -> rule2)) -> rule7))] Bob is round.[(((triple6) -> rule5) OR ((triple7 triple8) -> rule4) OR ((((triple7 triple8) -> rule6)) -> rule5) OR ((triple7 ((triple6) -> rule1)) -> rule4))] Charlie is quiet.[(((triple10) -> rule2))] @2: Charlie is big.[(((((triple10) -> rule2)) -> rule7))] Charlie is white.[(((((triple10) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple4) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple3) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple7 triple8) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7 triple8) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
triple8
((triple6) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Anne is white.
("Anne" "is" "white" "+")
((triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple6) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7 triple8) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple7 triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple6) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple7 triple8) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple7 triple8) -> (rule6 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((triple7 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple10) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2