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