Charlie is cold. Charlie is white. Gary is cold. Gary is quiet. Gary is red. Gary is young. Harry is cold. Harry is quiet. Harry is red. Harry is white. Green things are cold. If Charlie is red and Charlie is big then Charlie is white. If Harry is quiet then Harry is cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Charlie is red and Charlie is big then Charlie is white.
((("Charlie" "is" "red" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "white" "+"))
If Harry is quiet then Harry is cold.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "cold" "+"))
Harry is red.
True
1
proof
[(triple9)]
("Harry" "is" "red" "+")
triple9
Harry is not cold.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule3))]
("Harry" "is" "cold" "-")
triple7
((triple8) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is cold.[(triple1)] Charlie is white.[(triple2)] Gary is cold.[(triple3)] Gary is quiet.[(triple4)] Gary is red.[(triple5)] Gary is young.[(triple6)] Harry is cold.[(triple7 OR ((triple8) -> rule3))] Harry is quiet.[(triple8)] Harry is red.[(triple9)] Harry is white.[(triple10)]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple8) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10