Bob is big. Bob is blue. Bob is kind. Bob is round. Bob is smart. Dave is big. Dave is quiet. Dave is red. Dave is round. Gary is big. Gary is blue. Gary is kind. Gary is quiet. Gary is red. Gary is round. Gary is smart. All red people are big. If Dave is blue then Dave is smart. All kind, big people are smart. Red people are kind. Big, quiet people are round. If someone is round then they are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Dave is blue then Dave is smart.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "smart" "+"))
All kind, big people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Big, quiet people are round.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Gary is kind.
True
1
proof
[(triple12 OR ((triple14) -> rule4) OR ((triple15) -> rule6) OR ((((triple10 triple13) -> rule5)) -> rule6) OR ((((((triple14) -> rule1) triple13) -> rule5)) -> rule6))]
("Gary" "is" "kind" "+")
triple12
((triple14) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple15) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple10 triple13) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple14) -> (rule1 % int3)) triple13) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Dave is kind.
True
2
proof
[(((triple8) -> rule4) OR ((triple9) -> rule6) OR ((((triple6 triple7) -> rule5)) -> rule6) OR ((((((triple8) -> rule1) triple7) -> rule5)) -> rule6))]
("Dave" "is" "kind" "+")
((triple8) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple6 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not kind.
False
2
inv-proof
[(((triple8) -> rule4) OR ((triple9) -> rule6) OR ((((triple6 triple7) -> rule5)) -> rule6) OR ((((((triple8) -> rule1) triple7) -> rule5)) -> rule6))]
("Dave" "is" "kind" "-")
((triple8) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple6 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
True
4
proof
[(((((triple8) -> rule4) triple6) -> rule3) OR ((((triple9) -> rule6) triple6) -> rule3) OR ((((triple8) -> rule4) ((triple8) -> rule1)) -> rule3) OR ((((triple9) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3))]
("Dave" "is" "smart" "+")
((((triple8) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple6 triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple6 triple7) -> (rule5 % int4))) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) ((triple8) -> (rule1 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not smart.
False
4
inv-proof
[(((((triple8) -> rule4) triple6) -> rule3) OR ((((triple9) -> rule6) triple6) -> rule3) OR ((((triple8) -> rule4) ((triple8) -> rule1)) -> rule3) OR ((((triple9) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3))]
("Dave" "is" "smart" "-")
((((triple8) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple6 triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple6 triple7) -> (rule5 % int4))) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) ((triple8) -> (rule1 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is kind.[(triple3 OR ((triple4) -> rule6))] Bob is round.[(triple4)] Bob is smart.[(triple5 OR ((triple3 triple1) -> rule3) OR ((((triple4) -> rule6) triple1) -> rule3))] Dave is big.[(triple6 OR ((triple8) -> rule1))] Dave is quiet.[(triple7)] Dave is red.[(triple8)] Dave is round.[(triple9 OR ((triple6 triple7) -> rule5) OR ((((triple8) -> rule1) triple7) -> rule5))] Gary is big.[(triple10 OR ((triple14) -> rule1))] Gary is blue.[(triple11)] Gary is kind.[(triple12 OR ((triple14) -> rule4) OR ((triple15) -> rule6) OR ((((triple10 triple13) -> rule5)) -> rule6) OR ((((((triple14) -> rule1) triple13) -> rule5)) -> rule6))] Gary is quiet.[(triple13)] Gary is red.[(triple14)] Gary is round.[(triple15 OR ((triple10 triple13) -> rule5) OR ((((triple14) -> rule1) triple13) -> rule5))] Gary is smart.[(triple16 OR ((triple12 triple10) -> rule3) OR ((triple12 ((triple14) -> rule1)) -> rule3) OR ((((triple14) -> rule4) triple10) -> rule3) OR ((((triple15) -> rule6) triple10) -> rule3) OR ((((triple14) -> rule4) ((triple14) -> rule1)) -> rule3) OR ((((triple15) -> rule6) ((triple14) -> rule1)) -> rule3) OR ((((((triple10 triple13) -> rule5)) -> rule6) triple10) -> rule3) OR ((((((triple10 triple13) -> rule5)) -> rule6) ((triple14) -> rule1)) -> rule3) OR ((((((((triple14) -> rule1) triple13) -> rule5)) -> rule6) triple10) -> rule3) OR ((((((((triple14) -> rule1) triple13) -> rule5)) -> rule6) ((triple14) -> rule1)) -> rule3))] @1: Dave is kind.[(((triple8) -> rule4) OR ((triple9) -> rule6) OR ((((triple6 triple7) -> rule5)) -> rule6) OR ((((((triple8) -> rule1) triple7) -> rule5)) -> rule6))] @2: Dave is smart.[(((((triple8) -> rule4) triple6) -> rule3) OR ((((triple9) -> rule6) triple6) -> rule3) OR ((((triple8) -> rule4) ((triple8) -> rule1)) -> rule3) OR ((((triple9) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((triple6 triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) triple6) -> rule3) OR ((((((((triple8) -> rule1) triple7) -> rule5)) -> rule6) ((triple8) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple3 triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple4) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple8) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple6 triple7) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple8) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple14) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
((triple14) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple15) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple10 triple13) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple14) -> (rule1 % int3)) triple13) -> (rule5 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
((triple10 triple13) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14) -> (rule1 % int2)) triple13) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple16
((triple12 triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple12 ((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple14) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple15) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple14) -> (rule4 % int3)) ((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((triple15) -> (rule6 % int3)) ((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple10 triple13) -> (rule5 % int3))) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple10 triple13) -> (rule5 % int4))) -> (rule6 % int3)) ((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((((((((triple14) -> (rule1 % int4)) triple13) -> (rule5 % int3))) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple14) -> (rule1 % int4)) triple13) -> (rule5 % int3))) -> (rule6 % int2)) ((triple14) -> (rule1 % int4))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((triple8) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple6 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((triple8) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple6 triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple6 triple7) -> (rule5 % int4))) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((((triple8) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule6 % int2)) ((triple8) -> (rule1 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4