Charlie is white. Erin is quiet. Erin is red. All green, quiet things are not kind. If something is kind and red then it is white. If something is red then it is white. If Erin is red and Erin is white then Erin is kind. Red things are not green. All white things are smart. If Charlie is furry and Charlie is kind then Charlie is white. If Charlie is smart and Charlie is not kind then Charlie is furry.
Charlie is white.
("Charlie" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
All green, quiet things are not kind.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
If something is kind and red then it is white.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Erin is red and Erin is white then Erin is kind.
((("Erin" "is" "red" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "kind" "+"))
Red things are not green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Charlie is furry and Charlie is kind then Charlie is white.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is smart and Charlie is not kind then Charlie is furry.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "furry" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Erin is not quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "-")
triple2
Erin is not green.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "green" "-")
((triple3) -> (rule5 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is kind.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "kind" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "kind" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is white.[(triple1)] Erin is quiet.[(triple2)] Erin is red.[(triple3)] @1: Charlie is smart.[(((triple1) -> rule6))] Erin is not green.[(((triple3) -> rule5))] Erin is white.[(((triple3) -> rule3))] @2: Erin is kind.[(((triple3 ((triple3) -> rule3)) -> rule4))] Erin is smart.[(((((triple3) -> rule3)) -> rule6))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
((triple3) -> (rule5 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2