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