Charlie is cold. Charlie is nice. Charlie is round. If Charlie is cold and Charlie is not nice then Charlie is round. If something is blue and not nice then it is not cold. All nice, cold things are blue. If something is nice then it is blue. Red things are not round. If something is cold and nice then it is not red.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If Charlie is cold and Charlie is not nice then Charlie is round.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "round" "+"))
If something is blue and not nice then it is not cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "cold" "-"))
All nice, cold things are blue.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Red things are not round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
If something is cold and nice then it is not red.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "-"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Charlie is blue.
True
2
proof
[(((triple2) -> rule4) OR ((triple2 triple1) -> rule3))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("Charlie" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is cold.[(triple1)] Charlie is nice.[(triple2)] Charlie is round.[(triple3)] @1: Charlie is blue.[(((triple2) -> rule4) OR ((triple2 triple1) -> rule3))] Charlie is not red.[(((triple1 triple2) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((triple1 triple2) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1