Anne is round. Dave is kind. Erin is nice. Gary is round. If Anne is kind then Anne is white. If something is furry and not round then it is not nice. If something is blue then it is nice. If something is red then it is white. White things are not furry. All round things are kind.
Anne is round.
("Anne" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
If Anne is kind then Anne is white.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "white" "+"))
If something is furry and not round then it is not nice.
((("something" "is" "furry" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "-"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
White things are not furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "-"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Erin is nice.
True
1
proof
[(triple3)]
("Erin" "is" "nice" "+")
triple3
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple4) -> rule6))]
("Gary" "is" "kind" "-")
((triple4) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Anne" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not furry.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
("Anne" "is" "furry" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
("Anne" "is" "furry" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "kind" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "nice" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is round.[(triple1)] Dave is kind.[(triple2)] Erin is nice.[(triple3)] Gary is round.[(triple4)] @1: Anne is kind.[(((triple1) -> rule6))] Gary is kind.[(((triple4) -> rule6))] @2: Anne is white.[(((((triple1) -> rule6)) -> rule1))] @3: Anne is not furry.[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not furry.
("Anne" "is" "furry" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3