Anne is big. Anne is green. Anne is kind. Anne is red. Anne is white. Dave is big. Dave is green. Dave is kind. Dave is red. Dave is smart. Kind, blue things are green. Red, blue things are green. Green, kind things are red. If Dave is red and Dave is smart then Dave is green. If something is green then it is blue. All big, red things are green. Red, big things are green. If Anne is smart and Anne is green then Anne is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Kind, blue things are green.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Red, blue things are green.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Green, kind things are red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Dave is red and Dave is smart then Dave is green.
((("Dave" "is" "red" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All big, red things are green.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Red, big things are green.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Anne is smart and Anne is green then Anne is blue.
((("Anne" "is" "smart" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "blue" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple2 triple3) -> rule3))]
("Anne" "is" "red" "+")
triple4
((triple2 triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not green.
False
1
inv-proof
[(triple2 OR ((triple1 triple4) -> rule6) OR ((triple4 triple1) -> rule7))]
("Anne" "is" "green" "-")
triple2
((triple1 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple1) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is blue.
True
2
proof
[(((triple7) -> rule5) OR ((((triple6 triple9) -> rule6)) -> rule5) OR ((((triple9 triple10) -> rule4)) -> rule5) OR ((((triple9 triple6) -> rule7)) -> rule5))]
("Dave" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple6 triple9) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple9 triple10) -> (rule4 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple9 triple6) -> (rule7 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is not blue.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple4 triple1) -> rule7)) -> rule5))]
("Anne" "is" "blue" "-")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple1 triple4) -> rule6) OR ((triple4 triple1) -> rule7))] Anne is kind.[(triple3)] Anne is red.[(triple4 OR ((triple2 triple3) -> rule3))] Anne is white.[(triple5)] Dave is big.[(triple6)] Dave is green.[(triple7 OR ((triple6 triple9) -> rule6) OR ((triple9 triple10) -> rule4) OR ((triple9 triple6) -> rule7))] Dave is kind.[(triple8)] Dave is red.[(triple9 OR ((triple7 triple8) -> rule3))] Dave is smart.[(triple10)] @1: Anne is blue.[(((triple2) -> rule5) OR ((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple4 triple1) -> rule7)) -> rule5))] Dave is blue.[(((triple7) -> rule5) OR ((((triple6 triple9) -> rule6)) -> rule5) OR ((((triple9 triple10) -> rule4)) -> rule5) OR ((((triple9 triple6) -> rule7)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple1) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple2 triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple6 triple9) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple9 triple10) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple9 triple6) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple7 triple8) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple6 triple9) -> (rule6 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple9 triple10) -> (rule4 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple9 triple6) -> (rule7 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2