Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is red. Gary is smart. Gary is white. Harry is kind. Harry is red. Harry is smart. White people are cold. If someone is kind and red then they are white.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind and red then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Harry is not smart.
False
1
inv-proof
[(triple10)]
("Harry" "is" "smart" "-")
triple10
Harry is white.
True
3
proof
[(((triple8 triple9) -> rule2))]
("Harry" "is" "white" "+")
((triple8 triple9) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
3
inv-proof
[(((triple8 triple9) -> rule2))]
("Harry" "is" "white" "-")
((triple8 triple9) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
True
4
proof
[(((((triple8 triple9) -> rule2)) -> rule1))]
("Harry" "is" "cold" "+")
((((triple8 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple8 triple9) -> rule2)) -> rule1))]
("Harry" "is" "cold" "-")
((((triple8 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Gary is big.[(triple1)] Gary is blue.[(triple2)] Gary is cold.[(triple3 OR ((triple7) -> rule1) OR ((((triple4 triple5) -> rule2)) -> rule1))] Gary is kind.[(triple4)] Gary is red.[(triple5)] Gary is smart.[(triple6)] Gary is white.[(triple7 OR ((triple4 triple5) -> rule2))] Harry is kind.[(triple8)] Harry is red.[(triple9)] Harry is smart.[(triple10)] @1: Harry is white.[(((triple8 triple9) -> rule2))] @2: Harry is cold.[(((((triple8 triple9) -> rule2)) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
((triple7) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple4 triple5) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
((triple8 triple9) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple8 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2