Charlie is kind. Charlie is red. Charlie is white. Gary is cold. Gary is green. Gary is kind. Gary is white. All smart, nice things are cold. If something is red then it is green. If Gary is green then Gary is not red. If Charlie is cold and Charlie is not nice then Charlie is kind. If Gary is green then Gary is kind. Green, nice things are white.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
All smart, nice things are cold.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Gary is green then Gary is not red.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "red" "-"))
If Charlie is cold and Charlie is not nice then Charlie is kind.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "kind" "+"))
If Gary is green then Gary is kind.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "kind" "+"))
Green, nice things are white.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Charlie is green.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "green" "+")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "green" "-")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is kind.[(triple1)] Charlie is red.[(triple2)] Charlie is white.[(triple3)] Gary is cold.[(triple4)] Gary is green.[(triple5)] Gary is kind.[(triple6 OR ((triple5) -> rule5))] Gary is white.[(triple7)] @1: Charlie is green.[(((triple2) -> rule2))] Gary is not red.[(((triple5) -> rule3))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
((triple5) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
((triple5) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1