Charlie is big. Charlie is not cold. Charlie is not nice. Erin is cold. Erin is not green. Erin is nice. Erin is red. Erin is white. Gary is quiet. Gary is white. If Gary is not red then Gary is white. All red people are cold. If Erin is green and Erin is not quiet then Erin is nice. If Gary is nice then Gary is big. All quiet, big people are green. All white people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is not red then Gary is white.
((("Gary" "is" "red" "~")) -> ("Gary" "is" "white" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Erin is green and Erin is not quiet then Erin is nice.
((("Erin" "is" "green" "+") ("Erin" "is" "quiet" "~")) -> ("Erin" "is" "nice" "+"))
If Gary is nice then Gary is big.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "big" "+"))
All quiet, big people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Erin is red.
True
1
proof
[(triple7)]
("Erin" "is" "red" "+")
triple7
Gary is not white.
False
1
inv-proof
[(triple10)]
("Gary" "is" "white" "-")
triple10
Gary is nice.
True
2
proof
[(((triple10) -> rule6))]
("Gary" "is" "nice" "+")
((triple10) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple10) -> rule6))]
("Gary" "is" "nice" "-")
((triple10) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
True
3
proof
[(((((triple10) -> rule6)) -> rule4))]
("Gary" "is" "big" "+")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple10) -> rule6)) -> rule4))]
("Gary" "is" "big" "-")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is green.
True
5
proof
[(((triple9 ((((triple10) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "green" "+")
((triple9 ((((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not green.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "green" "-")
((triple9 ((((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "green" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
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" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is not cold.[(triple2)] Charlie is not nice.[(triple3)] Erin is cold.[(triple4 OR ((triple7) -> rule2))] Erin is nice.[(triple6 OR ((triple8) -> rule6))] Erin is not green.[(triple5)] Erin is red.[(triple7)] Erin is white.[(triple8)] Gary is quiet.[(triple9)] Gary is white.[(triple10)] @1: Gary is nice.[(((triple10) -> rule6))] @2: Gary is big.[(((((triple10) -> rule6)) -> rule4))] @3: Gary is green.[(((triple9 ((((triple10) -> rule6)) -> rule4)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((triple7) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple6
((triple8) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
((triple10) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple9 ((((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3