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