Charlie is white. Erin is white. All quiet, red people are big. All white people are furry. Blue people are white. If someone is blue then they are red. If Charlie is rough and Charlie is not blue then Charlie is furry. If Erin is furry then Erin is blue.
Charlie is white.
("Charlie" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
All quiet, red people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Charlie is rough and Charlie is not blue then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "furry" "+"))
If Erin is furry then Erin is blue.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "blue" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Charlie is furry.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Erin" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("Erin" "is" "blue" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("Erin" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("Erin" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is white.[(triple1)] Erin is white.[(triple2)] @1: Charlie is furry.[(((triple1) -> rule2))] Erin is furry.[(((triple2) -> rule2))] @2: Erin is blue.[(((((triple2) -> rule2)) -> rule6))] @3: Erin is red.[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3