Charlie is not red. Gary is nice. Gary is not red. All young things are red. If something is green and big then it is round. If something is red and big then it is round. If Charlie is nice and Charlie is big then Charlie is not red. If Gary is green then Gary is big. If something is red and not green then it is young. If something is green and not red then it is not cold. All nice things are not cold.
Charlie is not red.
("Charlie" "is" "red" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not red.
("Gary" "is" "red" "-")
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is green and big then it is round.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is red and big then it is round.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Charlie is nice and Charlie is big then Charlie is not red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "-"))
If Gary is green then Gary is big.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "big" "+"))
If something is red and not green then it is young.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
If something is green and not red then it is not cold.
((("something" "is" "green" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "-"))
All nice things are not cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
Charlie is not red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Charlie is red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Gary is not cold.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "cold" "-")
((triple2) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is cold.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is not red.[(triple1)] Gary is nice.[(triple2)] Gary is not red.[(triple3)] @1: Gary is not cold.[(((triple2) -> rule8))]
Charlie is not red.
("Charlie" "is" "red" "-")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is not red.
("Gary" "is" "red" "-")
triple3
Gary is not cold.
("Gary" "is" "cold" "-")
((triple2) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1