Anne is big. Anne is furry. Anne is green. Anne is kind. Anne is smart. Charlie is big. Charlie is furry. Charlie is kind. Charlie is smart. Charlie is white. Harry is furry. Harry is green. Harry is kind. Harry is smart. Harry is white. All green things are big. Kind things are furry. If Anne is smart and Anne is white then Anne is furry. If Harry is furry then Harry is white. If Anne is kind then Anne is green. If Anne is green and Anne is blue then Anne is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Anne is smart and Anne is white then Anne is furry.
((("Anne" "is" "smart" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "furry" "+"))
If Harry is furry then Harry is white.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "white" "+"))
If Anne is kind then Anne is green.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "green" "+"))
If Anne is green and Anne is blue then Anne is kind.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple13)]
("Harry" "is" "kind" "+")
triple13
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1) OR ((((triple4) -> rule5)) -> rule1))]
("Anne" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Harry is big.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "big" "+")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple12) -> rule1))]
("Harry" "is" "big" "-")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule1) OR ((((triple4) -> rule5)) -> rule1))] Anne is furry.[(triple2 OR ((triple4) -> rule2))] Anne is green.[(triple3 OR ((triple4) -> rule5))] Anne is kind.[(triple4)] Anne is smart.[(triple5)] Charlie is big.[(triple6)] Charlie is furry.[(triple7 OR ((triple8) -> rule2))] Charlie is kind.[(triple8)] Charlie is smart.[(triple9)] Charlie is white.[(triple10)] Harry is furry.[(triple11 OR ((triple13) -> rule2))] Harry is green.[(triple12)] Harry is kind.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15 OR ((triple11) -> rule4) OR ((((triple13) -> rule2)) -> rule4))] @1: Harry is big.[(((triple12) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple4) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple13) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple11) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1