Bob is green. Erin is big. Erin is green. If something is round and not blue then it is furry. All big things are round. If Erin is round and Erin is blue then Erin is not green.
Bob is green.
("Bob" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
If something is round and not blue then it is furry.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "furry" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Erin is round and Erin is blue then Erin is not green.
((("Erin" "is" "round" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "green" "-"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Erin is round.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "round" "+")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "round" "-")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is green.[(triple1)] Erin is big.[(triple2)] Erin is green.[(triple3)] @1: Erin is round.[(((triple2) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1