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