Charlie is blue. Charlie is furry. Charlie is kind. Charlie is rough. Dave is blue. Dave is furry. Dave is nice. Dave is white. Erin is furry. Erin is white. If something is blue and white then it is cold. If Charlie is blue then Charlie is white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is blue and white then it is cold.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Charlie is blue then Charlie is white.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "white" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Dave is cold.
True
3
proof
[(((triple5 triple8) -> rule1))]
("Dave" "is" "cold" "+")
((triple5 triple8) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "white" "-")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Charlie is rough.[(triple4)] Dave is blue.[(triple5)] Dave is furry.[(triple6)] Dave is nice.[(triple7)] Dave is white.[(triple8)] Erin is furry.[(triple9)] Erin is white.[(triple10)] @1: Charlie is white.[(((triple1) -> rule2))] Dave is cold.[(((triple5 triple8) -> rule1))] @2: Charlie is cold.[(((triple1 ((triple1) -> rule2)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple5 triple8) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2