Anne is nice. Bob is furry. Charlie is quiet. Erin is blue. Nice people are quiet. All nice, green people are furry. If someone is green and not nice then they are furry. If Anne is green then Anne is quiet. If someone is nice and quiet then they are green. If Charlie is blue then Charlie is quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All nice, green people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is green and not nice then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
If Anne is green then Anne is quiet.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is nice and quiet then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Charlie is blue then Charlie is quiet.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "furry" "+")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not furry.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "furry" "-")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "green" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Bob is furry.[(triple2)] Charlie is quiet.[(triple3)] Erin is blue.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule1))] @2: Anne is green.[(((triple1 ((triple1) -> rule1)) -> rule5))] @3: Anne is furry.[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3