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