Bob is furry. Bob is round. Bob is white. Erin is furry. Erin is quiet. Harry is quiet. Harry is white. If someone is round then they are nice. All white, furry people are nice. Furry people are quiet. All nice people are quiet. If someone is quiet and furry then they are green. Green, quiet people are white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All white, furry people are nice.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and furry then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Green, quiet people are white.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Erin is furry.
True
1
proof
[(triple4)]
("Erin" "is" "furry" "+")
triple4
Erin is not quiet.
False
1
inv-proof
[(triple5 OR ((triple4) -> rule3))]
("Erin" "is" "quiet" "-")
triple5
((triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Bob is nice.
True
2
proof
[(((triple2) -> rule1) OR ((triple3 triple1) -> rule2) OR ((((((((triple1) -> rule3) triple1) -> rule5) ((triple1) -> rule3)) -> rule6) triple1) -> rule2))]
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3)) ((triple1) -> (rule3 % int4))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2) -> rule1)) -> rule4) OR ((((triple3 triple1) -> rule2)) -> rule4))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is white.
True
5
proof
[(((((triple5 triple4) -> rule5) triple5) -> rule6) OR ((((triple5 triple4) -> rule5) ((triple4) -> rule3)) -> rule6) OR ((((((triple4) -> rule3) triple4) -> rule5) triple5) -> rule6) OR ((((((triple4) -> rule3) triple4) -> rule5) ((triple4) -> rule3)) -> rule6))]
("Erin" "is" "white" "+")
((((triple5 triple4) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple5 triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple4) -> (rule3 % int3)) triple4) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple4) -> (rule3 % int3)) triple4) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule5) OR ((((((triple2) -> rule1)) -> rule4) triple1) -> rule5) OR ((((((triple3 triple1) -> rule2)) -> rule4) triple1) -> rule5))]
("Bob" "is" "green" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple3 triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Erin is nice.
True
7
proof
[(((((((triple5 triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((triple5 triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2))]
("Erin" "is" "nice" "+")
((((((triple5 triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple5 triple4) -> (rule5 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int4))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is not nice.
False
7
inv-proof
[(((((((triple5 triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((triple5 triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2))]
("Erin" "is" "nice" "-")
((((((triple5 triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple5 triple4) -> (rule5 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int4))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is furry.[(triple1)] Bob is round.[(triple2)] Bob is white.[(triple3 OR ((((((triple1) -> rule3) triple1) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule3) triple1) -> rule5) ((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule4) triple1) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule4) triple1) -> rule5) ((((triple2) -> rule1)) -> rule4)) -> rule6))] Erin is furry.[(triple4)] Erin is quiet.[(triple5 OR ((triple4) -> rule3))] Harry is quiet.[(triple6)] Harry is white.[(triple7)] @1: Bob is nice.[(((triple2) -> rule1) OR ((triple3 triple1) -> rule2) OR ((((((((triple1) -> rule3) triple1) -> rule5) ((triple1) -> rule3)) -> rule6) triple1) -> rule2))] Bob is quiet.[(((triple1) -> rule3) OR ((((triple2) -> rule1)) -> rule4) OR ((((triple3 triple1) -> rule2)) -> rule4))] Erin is green.[(((triple5 triple4) -> rule5) OR ((((triple4) -> rule3) triple4) -> rule5))] @2: Bob is green.[(((((triple1) -> rule3) triple1) -> rule5) OR ((((((triple2) -> rule1)) -> rule4) triple1) -> rule5) OR ((((((triple3 triple1) -> rule2)) -> rule4) triple1) -> rule5))] Erin is white.[(((((triple5 triple4) -> rule5) triple5) -> rule6) OR ((((triple5 triple4) -> rule5) ((triple4) -> rule3)) -> rule6) OR ((((((triple4) -> rule3) triple4) -> rule5) triple5) -> rule6) OR ((((((triple4) -> rule3) triple4) -> rule5) ((triple4) -> rule3)) -> rule6))] @3: Erin is nice.[(((((((triple5 triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((triple5 triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) triple5) -> rule6) triple4) -> rule2) OR ((((((((triple4) -> rule3) triple4) -> rule5) ((triple4) -> rule3)) -> rule6) triple4) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3)) ((((triple2) -> (rule1 % int2))) -> (rule4 % int4))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule5 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3)) ((triple1) -> (rule3 % int4))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple5 triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple3 triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((triple5 triple4) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple5 triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple4) -> (rule3 % int3)) triple4) -> (rule5 % int2)) triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple4) -> (rule3 % int3)) triple4) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple5 triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple5 triple4) -> (rule5 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int4))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4