Anne is furry. Anne is nice. Anne is quiet. Anne is red. Anne is round. Anne is white. Anne is young. Erin is furry. Erin is nice. Erin is quiet. Erin is red. Erin is round. Erin is white. Erin is young. If something is red then it is furry. If Anne is white and Anne is furry then Anne is nice. If something is young then it is quiet. All quiet, red things are young. If Erin is red then Erin is quiet. Red, round things are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Anne is white and Anne is furry then Anne is nice.
((("Anne" "is" "white" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "nice" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All quiet, red things are young.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Erin is red then Erin is quiet.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "quiet" "+"))
Red, round things are quiet.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Anne is white.
True
1
proof
[(triple6)]
("Anne" "is" "white" "+")
triple6
Erin is not quiet.
False
1
inv-proof
[(triple10 OR ((triple11) -> rule5) OR ((triple14) -> rule3) OR ((triple11 triple12) -> rule6))]
("Erin" "is" "quiet" "-")
triple10
((triple11) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple14) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
@0: Anne is furry.[(triple1 OR ((triple4) -> rule1))] Anne is nice.[(triple2 OR ((triple6 triple1) -> rule2) OR ((triple6 ((triple4) -> rule1)) -> rule2))] Anne is quiet.[(triple3 OR ((triple7) -> rule3) OR ((triple4 triple5) -> rule6))] Anne is red.[(triple4)] Anne is round.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7 OR ((triple3 triple4) -> rule4) OR ((((triple4 triple5) -> rule6) triple4) -> rule4))] Erin is furry.[(triple8 OR ((triple11) -> rule1))] Erin is nice.[(triple9)] Erin is quiet.[(triple10 OR ((triple11) -> rule5) OR ((triple14) -> rule3) OR ((triple11 triple12) -> rule6))] Erin is red.[(triple11)] Erin is round.[(triple12)] Erin is white.[(triple13)] Erin is young.[(triple14 OR ((triple10 triple11) -> rule4) OR ((((triple11) -> rule5) triple11) -> rule4) OR ((((triple11 triple12) -> rule6) triple11) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple6 triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple6 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple7) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple3 triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple4 triple5) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple8
((triple11) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
((triple11) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple14) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple10 triple11) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple11) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple11 triple12) -> (rule6 % int2)) triple11) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2