Erin is kind. Erin is nice. Erin is round. Gary is big. Gary is nice. Gary is quiet. Gary is red. All cold people are quiet. Nice people are quiet. All kind, cold people are red. All nice, quiet people are big. All quiet people are cold. Red people are quiet.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All kind, cold people are red.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All nice, quiet people are big.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Erin is round.
True
1
proof
[(triple3)]
("Erin" "is" "round" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple4 OR ((triple5 triple6) -> rule4) OR ((triple5 ((triple5) -> rule2)) -> rule4) OR ((triple5 ((triple7) -> rule6)) -> rule4))]
("Gary" "is" "big" "-")
triple4
((triple5 triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple5 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Erin is kind.[(triple1)] Erin is nice.[(triple2)] Erin is round.[(triple3)] Gary is big.[(triple4 OR ((triple5 triple6) -> rule4) OR ((triple5 ((triple5) -> rule2)) -> rule4) OR ((triple5 ((triple7) -> rule6)) -> rule4))] Gary is nice.[(triple5)] Gary is quiet.[(triple6 OR ((triple5) -> rule2) OR ((triple7) -> rule6))] Gary is red.[(triple7)] @1: Erin is quiet.[(((triple2) -> rule2))] Gary is cold.[(((triple6) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] @2: Erin is big.[(((triple2 ((triple2) -> rule2)) -> rule4))] Erin is cold.[(((((triple2) -> rule2)) -> rule5))] @3: Erin is red.[(((triple1 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
((triple5 triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple5 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
((triple5) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple7) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple6) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple1 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3