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