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