Harry is cold. Harry is quiet. Harry is white. If something is quiet and not green then it is white. All quiet things are cold. If something is white and red then it is cold. If something is round then it is cold. If something is smart and not green then it is red. All quiet things are red.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is quiet and not green then it is white.
((("something" "is" "quiet" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is white and red then it is cold.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not green then it is red.
((("something" "is" "smart" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Harry is quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule2) OR ((triple3 ((triple2) -> rule6)) -> rule3))]
("Harry" "is" "cold" "-")
triple1
((triple2) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Harry is cold.[(triple1 OR ((triple2) -> rule2) OR ((triple3 ((triple2) -> rule6)) -> rule3))] Harry is quiet.[(triple2)] Harry is white.[(triple3)] @1: Harry is red.[(((triple2) -> rule6))]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
((triple2) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1