Charlie is blue. Charlie is cold. Dave is rough. Erin is green. Erin is quiet. Erin is rough. Erin is young. If Erin is young then Erin is blue. All quiet, blue things are cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is young then Erin is blue.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "blue" "+"))
All quiet, blue things are cold.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Erin is blue.
True
2
proof
[(((triple7) -> rule1))]
("Erin" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple7) -> rule1))]
("Erin" "is" "blue" "-")
((triple7) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
True
4
proof
[(((triple5 ((triple7) -> rule1)) -> rule2))]
("Erin" "is" "cold" "+")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((triple5 ((triple7) -> rule1)) -> rule2))]
("Erin" "is" "cold" "-")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Dave is rough.[(triple3)] Erin is green.[(triple4)] Erin is quiet.[(triple5)] Erin is rough.[(triple6)] Erin is young.[(triple7)] @1: Erin is blue.[(((triple7) -> rule1))] @2: Erin is cold.[(((triple5 ((triple7) -> rule1)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2