Charlie is big. Charlie is cold. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is white. Dave is rough. Erin is big. Erin is nice. Erin is quiet. Erin is red. Erin is rough. Gary is red. Gary is rough. Gary is white. White people are red. If someone is red and white then they are big. If someone is quiet and big then they are cold. All rough people are quiet. If someone is cold then they are big. If Dave is quiet then Dave is white. If someone is red and nice then they are cold. All quiet, red people are rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is red and white then they are big.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and big then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Dave is quiet then Dave is white.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "white" "+"))
If someone is red and nice then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All quiet, red people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Erin is quiet.
True
1
proof
[(triple11 OR ((triple13) -> rule4))]
("Erin" "is" "quiet" "+")
triple11
((triple13) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Erin is cold.
True
3
proof
[(((triple11 triple9) -> rule3) OR ((triple12 triple10) -> rule7) OR ((((triple13) -> rule4) triple9) -> rule3))]
("Erin" "is" "cold" "+")
((triple11 triple9) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple12 triple10) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple13) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is not big.
False
3
inv-proof
[(((triple14 triple16) -> rule2) OR ((((triple16) -> rule1) triple16) -> rule2))]
("Gary" "is" "big" "-")
((triple14 triple16) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple16) -> (rule1 % int2)) triple16) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Dave is white.
True
3
proof
[(((((triple8) -> rule4)) -> rule6))]
("Dave" "is" "white" "+")
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not cold.
False
6
inv-proof
[(((((triple15) -> rule4) ((triple14 triple16) -> rule2)) -> rule3) OR ((((triple15) -> rule4) ((((triple16) -> rule1) triple16) -> rule2)) -> rule3))]
("Gary" "is" "cold" "-")
((((triple15) -> (rule4 % int3)) ((triple14 triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple15) -> (rule4 % int4)) ((((triple16) -> (rule1 % int3)) triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Dave is red.
True
4
proof
[(((((((triple8) -> rule4)) -> rule6)) -> rule1))]
("Dave" "is" "red" "+")
((((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple8) -> rule4)) -> rule6)) -> rule1))]
("Dave" "is" "red" "-")
((((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
True
8
proof
[(((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2))]
("Dave" "is" "big" "+")
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is not big.
False
8
inv-proof
[(((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2))]
("Dave" "is" "big" "-")
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is cold.
True
11
proof
[(((((triple8) -> rule4) ((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple8) -> (rule4 % int5)) ((((((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
Dave is not cold.
False
11
inv-proof
[(((((triple8) -> rule4) ((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2)) -> rule3))]
("Dave" "is" "cold" "-")
((((triple8) -> (rule4 % int5)) ((((((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule5) OR ((triple5 triple7) -> rule2) OR ((((triple5 triple3) -> rule7)) -> rule5) OR ((((triple7) -> rule1) triple7) -> rule2) OR ((((((triple7) -> rule1) triple3) -> rule7)) -> rule5))] Charlie is cold.[(triple2 OR ((triple4 triple1) -> rule3) OR ((triple5 triple3) -> rule7) OR ((triple4 ((triple5 triple7) -> rule2)) -> rule3) OR ((((triple6) -> rule4) triple1) -> rule3) OR ((((triple7) -> rule1) triple3) -> rule7) OR ((((triple6) -> rule4) ((triple5 triple7) -> rule2)) -> rule3) OR ((triple4 ((((triple7) -> rule1) triple7) -> rule2)) -> rule3) OR ((((triple6) -> rule4) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3))] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4 OR ((triple6) -> rule4))] Charlie is red.[(triple5 OR ((triple7) -> rule1))] Charlie is rough.[(triple6 OR ((triple4 triple5) -> rule8) OR ((triple4 ((triple7) -> rule1)) -> rule8))] Charlie is white.[(triple7)] Dave is rough.[(triple8)] Erin is big.[(triple9 OR ((((triple12 triple10) -> rule7)) -> rule5))] Erin is nice.[(triple10)] Erin is quiet.[(triple11 OR ((triple13) -> rule4))] Erin is red.[(triple12)] Erin is rough.[(triple13 OR ((triple11 triple12) -> rule8))] Gary is red.[(triple14 OR ((triple16) -> rule1))] Gary is rough.[(triple15)] Gary is white.[(triple16)] @1: Dave is quiet.[(((triple8) -> rule4))] Erin is cold.[(((triple11 triple9) -> rule3) OR ((triple12 triple10) -> rule7) OR ((((triple13) -> rule4) triple9) -> rule3))] Gary is big.[(((triple14 triple16) -> rule2) OR ((((triple16) -> rule1) triple16) -> rule2))] Gary is quiet.[(((triple15) -> rule4))] @2: Dave is white.[(((((triple8) -> rule4)) -> rule6))] Gary is cold.[(((((triple15) -> rule4) ((triple14 triple16) -> rule2)) -> rule3) OR ((((triple15) -> rule4) ((((triple16) -> rule1) triple16) -> rule2)) -> rule3))] @3: Dave is red.[(((((((triple8) -> rule4)) -> rule6)) -> rule1))] @4: Dave is big.[(((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2))] @5: Dave is cold.[(((((triple8) -> rule4) ((((((((triple8) -> rule4)) -> rule6)) -> rule1) ((((triple8) -> rule4)) -> rule6)) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple5 triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple7) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple7) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple5 triple3) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple4 ((triple5 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple6) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple7) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple5 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple4 ((((triple7) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((triple6) -> (rule4 % int4)) ((((triple7) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple4 triple5) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 ((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple9
((((triple12 triple10) -> (rule7 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
((triple13) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
((triple11 triple12) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple16) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Gary is white.
("Gary" "is" "white" "+")
triple16
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple8) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple11 triple9) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple12 triple10) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple13) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple14 triple16) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple16) -> (rule1 % int2)) triple16) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple15) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple15) -> (rule4 % int3)) ((triple14 triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple15) -> (rule4 % int4)) ((((triple16) -> (rule1 % int3)) triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
((((triple8) -> (rule4 % int5)) ((((((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple8) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5