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