Anne is big. Anne is green. Anne is red. Anne is smart. Anne is young. Charlie is blue. Charlie is cold. Charlie is green. Charlie is smart. Harry is big. Harry is blue. Harry is green. Harry is red. Harry is smart. Harry is young. If Harry is blue then Harry is big. Green people are cold. If someone is green and cold then they are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is blue then Harry is big.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "big" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and cold then they are red.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple11)]
("Harry" "is" "blue" "-")
triple11
Anne is cold.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple12) -> rule2))]
("Harry" "is" "cold" "-")
((triple12) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is red.[(triple3 OR ((triple2 ((triple2) -> rule2)) -> rule3))] Anne is smart.[(triple4)] Anne is young.[(triple5)] Charlie is blue.[(triple6)] Charlie is cold.[(triple7 OR ((triple8) -> rule2))] Charlie is green.[(triple8)] Charlie is smart.[(triple9)] Harry is big.[(triple10 OR ((triple11) -> rule1))] Harry is blue.[(triple11)] Harry is green.[(triple12)] Harry is red.[(triple13 OR ((triple12 ((triple12) -> rule2)) -> rule3))] Harry is smart.[(triple14)] Harry is young.[(triple15)] @1: Anne is cold.[(((triple2) -> rule2))] Charlie is red.[(((triple8 triple7) -> rule3) OR ((triple8 ((triple8) -> rule2)) -> rule3))] Harry is cold.[(((triple12) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple11) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple8 triple7) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple12) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1