Anne is big. Anne is not cold. Anne is green. Anne is not white. Gary is big. Gary is not cold. Gary is furry. Gary is green. Gary is smart. Gary is white. Harry is big. Harry is blue. Harry is furry. Harry is not green. Harry is smart. If something is smart and not green then it is white.
Anne is big.
("Anne" "is" "big" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is not white.
("Anne" "is" "white" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and not green then it is white.
((("something" "is" "smart" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "+"))
Harry is furry.
True
1
proof
[(triple13)]
("Harry" "is" "furry" "+")
triple13
Anne is white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "+")
triple4
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple3)] Anne is not cold.[(triple2)] Anne is not white.[(triple4)] Gary is big.[(triple5)] Gary is furry.[(triple7)] Gary is green.[(triple8)] Gary is not cold.[(triple6)] Gary is smart.[(triple9)] Gary is white.[(triple10)] Harry is big.[(triple11)] Harry is blue.[(triple12)] Harry is furry.[(triple13)] Harry is not green.[(triple14)] Harry is smart.[(triple15)] @1: Harry is white.[(((triple15 triple14) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is not cold.
("Gary" "is" "cold" "-")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is not green.
("Harry" "is" "green" "-")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1