Charlie is big. Dave is big. Erin is cold. If someone is green then they are blue. If someone is cold then they are blue. If Charlie is blue and Charlie is green then Charlie is kind.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is blue and Charlie is green then Charlie is kind.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "kind" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Erin is blue.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "kind" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Charlie is big.[(triple1)] Dave is big.[(triple2)] Erin is cold.[(triple3)] @1: Erin is blue.[(((triple3) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1