Anne is blue. Anne is green. Anne is red. Anne is white. Anne is young. Charlie is blue. Charlie is white. Charlie is young. Erin is blue. Erin is green. Erin is kind. Erin is white. Kind, green things are white. Green, blue things are red. If Erin is kind then Erin is young. All cold things are red. Cold, green things are young. If Erin is white and Erin is blue then Erin is red. Blue things are green. All kind, red things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Kind, green things are white.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Green, blue things are red.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If Erin is kind then Erin is young.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "young" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Cold, green things are young.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Erin is white and Erin is blue then Erin is red.
((("Erin" "is" "white" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "red" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All kind, red things are blue.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Anne is white.
True
1
proof
[(triple4)]
("Anne" "is" "white" "+")
triple4
Erin is not green.
False
1
inv-proof
[(triple10 OR ((triple9) -> rule7))]
("Erin" "is" "green" "-")
triple10
((triple9) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
True
3
proof
[(((triple10 triple9) -> rule2) OR ((triple12 triple9) -> rule6) OR ((((triple9) -> rule7) triple9) -> rule2) OR ((((triple11 triple10) -> rule1) triple9) -> rule6) OR ((((triple11 ((triple9) -> rule7)) -> rule1) triple9) -> rule6))]
("Erin" "is" "red" "+")
((triple10 triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple12 triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple9) -> (rule7 % int2)) triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple11 triple10) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple11 ((triple9) -> (rule7 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Charlie is not green.
False
2
inv-proof
[(((triple6) -> rule7))]
("Charlie" "is" "green" "-")
((triple6) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
True
4
proof
[(((((triple6) -> rule7) triple6) -> rule2))]
("Charlie" "is" "red" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple6) -> rule7) triple6) -> rule2))]
("Charlie" "is" "red" "-")
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule7))] Anne is red.[(triple3 OR ((triple2 triple1) -> rule2) OR ((((triple1) -> rule7) triple1) -> rule2))] Anne is white.[(triple4)] Anne is young.[(triple5)] Charlie is blue.[(triple6)] Charlie is white.[(triple7)] Charlie is young.[(triple8)] Erin is blue.[(triple9)] Erin is green.[(triple10 OR ((triple9) -> rule7))] Erin is kind.[(triple11)] Erin is white.[(triple12 OR ((triple11 triple10) -> rule1) OR ((triple11 ((triple9) -> rule7)) -> rule1))] @1: Charlie is green.[(((triple6) -> rule7))] Erin is red.[(((triple10 triple9) -> rule2) OR ((triple12 triple9) -> rule6) OR ((((triple9) -> rule7) triple9) -> rule2) OR ((((triple11 triple10) -> rule1) triple9) -> rule6) OR ((((triple11 ((triple9) -> rule7)) -> rule1) triple9) -> rule6))] Erin is young.[(((triple11) -> rule3))] @2: Charlie is red.[(((((triple6) -> rule7) triple6) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2 triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
((triple9) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple11 triple10) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple11 ((triple9) -> (rule7 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((triple6) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple10 triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple12 triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple9) -> (rule7 % int2)) triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple11 triple10) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple11 ((triple9) -> (rule7 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((triple11) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2