Charlie is round. Gary is cold. Gary is quiet. Quiet, round people are red. Quiet people are round. All cold, white people are big. White, big people are cold. All cold people are round. If someone is red then they are big. If someone is white and round then they are red. All cold people are kind.
Charlie is round.
("Charlie" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Quiet, round people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All cold, white people are big.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
White, big people are cold.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is white and round then they are red.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "round" "-")
triple1
Gary is kind.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "kind" "-")
((triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
True
4
proof
[(((triple3 ((triple2) -> rule5)) -> rule1) OR ((triple3 ((triple3) -> rule2)) -> rule1))]
("Gary" "is" "red" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not red.
False
4
inv-proof
[(((triple3 ((triple2) -> rule5)) -> rule1) OR ((triple3 ((triple3) -> rule2)) -> rule1))]
("Gary" "is" "red" "-")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
True
5
proof
[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule6) OR ((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule6))]
("Gary" "is" "big" "+")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not big.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule6) OR ((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule6))]
("Gary" "is" "big" "-")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is round.[(triple1)] Gary is cold.[(triple2)] Gary is quiet.[(triple3)] @1: Gary is kind.[(((triple2) -> rule8))] Gary is round.[(((triple2) -> rule5) OR ((triple3) -> rule2))] @2: Gary is red.[(((triple3 ((triple2) -> rule5)) -> rule1) OR ((triple3 ((triple3) -> rule2)) -> rule1))] @3: Gary is big.[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule6) OR ((((triple3 ((triple3) -> rule2)) -> rule1)) -> rule6))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple2) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3