Anne is big. Anne is kind. Anne is nice. Anne is rough. Bob is blue. Bob is kind. Bob is nice. Bob is red. Bob is rough. Dave is big. Dave is kind. Dave is nice. Dave is red. Dave is rough. Dave is round. All nice, big things are round. If something is round and big then it is red. Rough, big things are kind. If something is nice then it is red. All blue things are round. Round, red things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
All nice, big things are round.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is round and big then it is red.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Rough, big things are kind.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Round, red things are big.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Bob is rough.
True
1
proof
[(triple9)]
("Bob" "is" "rough" "+")
triple9
Bob is not rough.
False
1
inv-proof
[(triple9)]
("Bob" "is" "rough" "-")
triple9
Anne is red.
True
2
proof
[(((triple3) -> rule4) OR ((((triple3 triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "red" "+")
((triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple3 triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((triple3 triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "red" "-")
((triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple3 triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is big.
True
4
proof
[(((((triple5) -> rule5) triple8) -> rule6) OR ((((triple5) -> rule5) ((triple7) -> rule4)) -> rule6))]
("Bob" "is" "big" "+")
((((triple5) -> (rule5 % int2)) triple8) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((triple5) -> rule5) triple8) -> rule6) OR ((((triple5) -> rule5) ((triple7) -> rule4)) -> rule6))]
("Bob" "is" "big" "-")
((((triple5) -> (rule5 % int2)) triple8) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "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)] Anne is kind.[(triple2 OR ((triple4 triple1) -> rule3))] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Bob is blue.[(triple5)] Bob is kind.[(triple6 OR ((triple9 ((((triple5) -> rule5) triple8) -> rule6)) -> rule3) OR ((triple9 ((((triple5) -> rule5) ((triple7) -> rule4)) -> rule6)) -> rule3))] Bob is nice.[(triple7)] Bob is red.[(triple8 OR ((triple7) -> rule4))] Bob is rough.[(triple9)] Dave is big.[(triple10 OR ((triple15 triple13) -> rule6) OR ((triple15 ((triple12) -> rule4)) -> rule6))] Dave is kind.[(triple11 OR ((triple14 triple10) -> rule3) OR ((triple14 ((triple15 triple13) -> rule6)) -> rule3) OR ((triple14 ((triple15 ((triple12) -> rule4)) -> rule6)) -> rule3))] Dave is nice.[(triple12)] Dave is red.[(triple13 OR ((triple12) -> rule4) OR ((triple15 triple10) -> rule2) OR ((((triple12 triple10) -> rule1) triple10) -> rule2))] Dave is rough.[(triple14)] Dave is round.[(triple15 OR ((triple12 triple10) -> rule1))] @1: Anne is red.[(((triple3) -> rule4) OR ((((triple3 triple1) -> rule1) triple1) -> rule2))] Anne is round.[(((triple3 triple1) -> rule1))] Bob is round.[(((triple5) -> rule5))] @2: Bob is big.[(((((triple5) -> rule5) triple8) -> rule6) OR ((((triple5) -> rule5) ((triple7) -> rule4)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((triple9 ((((triple5) -> (rule5 % int3)) triple8) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((triple9 ((((triple5) -> (rule5 % int4)) ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple8
((triple7) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
((triple15 triple13) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple15 ((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple11
((triple14 triple10) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple14 ((triple15 triple13) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple14 ((triple15 ((triple12) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
triple13
((triple12) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple15 triple10) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple12 triple10) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple14
Dave is round.
("Dave" "is" "round" "+")
triple15
((triple12 triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple3 triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple5) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple5) -> (rule5 % int2)) triple8) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3