Charlie is blue. Charlie is kind. Charlie is nice. Charlie is rough. Dave is big. Dave is blue. Dave is furry. Dave is kind. Gary is big. Gary is blue. Gary is furry. Gary is kind. Gary is nice. Gary is red. Gary is rough. Kind, big people are red. If someone is furry and nice then they are kind. Furry people are big. If Gary is big then Gary is red. If someone is rough and red then they are big. Nice people are furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Kind, big people are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and nice then they are kind.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If Gary is big then Gary is red.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "red" "+"))
If someone is rough and red then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Dave is kind.
True
1
proof
[(triple8)]
("Dave" "is" "kind" "+")
triple8
Gary is not big.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule3) OR ((triple15 triple14) -> rule5) OR ((((triple13) -> rule6)) -> rule3))]
("Gary" "is" "big" "-")
triple9
((triple11) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple15 triple14) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is furry.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple8 triple5) -> rule1) OR ((triple8 ((triple7) -> rule3)) -> rule1))]
("Dave" "is" "red" "-")
((triple8 triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple8 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is big.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
True
5
proof
[(((triple2 ((((triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple3) -> rule6) triple3) -> rule2) ((((triple3) -> rule6)) -> rule3)) -> rule1))]
("Charlie" "is" "red" "+")
((triple2 ((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3)) ((((triple3) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is not red.
False
5
inv-proof
[(((triple2 ((((triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple3) -> rule6) triple3) -> rule2) ((((triple3) -> rule6)) -> rule3)) -> rule1))]
("Charlie" "is" "red" "-")
((triple2 ((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3)) ((((triple3) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2 OR ((((triple3) -> rule6) triple3) -> rule2))] Charlie is nice.[(triple3)] Charlie is rough.[(triple4)] Dave is big.[(triple5 OR ((triple7) -> rule3))] Dave is blue.[(triple6)] Dave is furry.[(triple7)] Dave is kind.[(triple8)] Gary is big.[(triple9 OR ((triple11) -> rule3) OR ((triple15 triple14) -> rule5) OR ((((triple13) -> rule6)) -> rule3))] Gary is blue.[(triple10)] Gary is furry.[(triple11 OR ((triple13) -> rule6))] Gary is kind.[(triple12 OR ((triple11 triple13) -> rule2) OR ((((triple13) -> rule6) triple13) -> rule2))] Gary is nice.[(triple13)] Gary is red.[(triple14 OR ((triple9) -> rule4) OR ((triple12 triple9) -> rule1) OR ((((triple11) -> rule3)) -> rule4) OR ((triple12 ((triple11) -> rule3)) -> rule1) OR ((((triple11 triple13) -> rule2) triple9) -> rule1) OR ((((triple11 triple13) -> rule2) ((triple11) -> rule3)) -> rule1) OR ((((((triple13) -> rule6)) -> rule3)) -> rule4) OR ((triple12 ((((triple13) -> rule6)) -> rule3)) -> rule1) OR ((((((triple13) -> rule6) triple13) -> rule2) triple9) -> rule1) OR ((((triple11 triple13) -> rule2) ((((triple13) -> rule6)) -> rule3)) -> rule1) OR ((((((triple13) -> rule6) triple13) -> rule2) ((triple11) -> rule3)) -> rule1) OR ((((((triple13) -> rule6) triple13) -> rule2) ((((triple13) -> rule6)) -> rule3)) -> rule1))] Gary is rough.[(triple15)] @1: Charlie is furry.[(((triple3) -> rule6))] Dave is red.[(((triple8 triple5) -> rule1) OR ((triple8 ((triple7) -> rule3)) -> rule1))] @2: Charlie is big.[(((((triple3) -> rule6)) -> rule3))] @3: Charlie is red.[(((triple2 ((((triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple3) -> rule6) triple3) -> rule2) ((((triple3) -> rule6)) -> rule3)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple7) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
((triple11) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple15 triple14) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
triple11
((triple13) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple12
((triple11 triple13) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple13) -> (rule6 % int2)) triple13) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple9) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple12 triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple12 ((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple11 triple13) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple11 triple13) -> (rule2 % int3)) ((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple13) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple12 ((((triple13) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple13) -> (rule6 % int3)) triple13) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple11 triple13) -> (rule2 % int4)) ((((triple13) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((triple13) -> (rule6 % int4)) triple13) -> (rule2 % int3)) ((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((((triple13) -> (rule6 % int4)) triple13) -> (rule2 % int3)) ((((triple13) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple8 triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple8 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3)) ((((triple3) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4