Anne is big. Anne is green. Anne is nice. Anne is quiet. Anne is red. Anne is round. Dave is green. Dave is kind. Dave is red. Dave is round. Harry is big. Harry is kind. Harry is nice. Harry is quiet. Harry is round. All quiet things are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Harry is nice.
True
1
proof
[(triple13)]
("Harry" "is" "nice" "+")
triple13
Dave is not green.
False
1
inv-proof
[(triple7)]
("Dave" "is" "green" "-")
triple7
Harry is red.
True
2
proof
[(((triple14) -> rule1))]
("Harry" "is" "red" "+")
((triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple14) -> rule1))]
("Harry" "is" "red" "-")
((triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is red.[(triple5 OR ((triple4) -> rule1))] Anne is round.[(triple6)] Dave is green.[(triple7)] Dave is kind.[(triple8)] Dave is red.[(triple9)] Dave is round.[(triple10)] Harry is big.[(triple11)] Harry is kind.[(triple12)] Harry is nice.[(triple13)] Harry is quiet.[(triple14)] Harry is round.[(triple15)] @1: Harry is red.[(((triple14) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple4) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is red.
("Harry" "is" "red" "+")
((triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1