Anne is furry. Anne is quiet. Anne is rough. Anne is young. Charlie is blue. Charlie is nice. Charlie is rough. Erin is big. Erin is furry. Erin is nice. Erin is quiet. Erin is rough. Blue people are big. If Anne is furry then Anne is nice. If someone is big then they are quiet. All blue, quiet people are young. If someone is quiet then they are blue. If someone is blue and furry then they are big. If someone is nice and furry then they are young. All furry, blue people are big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Anne is furry then Anne is nice.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "nice" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All blue, quiet people are young.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and furry then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and furry then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All furry, blue people are big.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "nice" "-")
triple6
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Anne is rough.[(triple3)] Anne is young.[(triple4 OR ((((triple1) -> rule2) triple1) -> rule7) OR ((((triple2) -> rule5) triple2) -> rule4))] Charlie is blue.[(triple5)] Charlie is nice.[(triple6)] Charlie is rough.[(triple7)] Erin is big.[(triple8 OR ((((triple11) -> rule5)) -> rule1) OR ((triple9 ((triple11) -> rule5)) -> rule8) OR ((((triple11) -> rule5) triple9) -> rule6))] Erin is furry.[(triple9)] Erin is nice.[(triple10)] Erin is quiet.[(triple11 OR ((triple8) -> rule3))] Erin is rough.[(triple12)] @1: Anne is blue.[(((triple2) -> rule5))] Anne is nice.[(((triple1) -> rule2))] Charlie is big.[(((triple5) -> rule1))] Erin is blue.[(((triple11) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] Erin is young.[(((triple10 triple9) -> rule7) OR ((((triple11) -> rule5) triple11) -> rule4) OR ((((triple11) -> rule5) ((triple8) -> rule3)) -> rule4) OR ((((((triple8) -> rule3)) -> rule5) triple11) -> rule4) OR ((((((triple8) -> rule3)) -> rule5) ((triple8) -> rule3)) -> rule4))] @2: Anne is big.[(((((triple2) -> rule5)) -> rule1) OR ((triple1 ((triple2) -> rule5)) -> rule8) OR ((((triple2) -> rule5) triple1) -> rule6))] Charlie is quiet.[(((((triple5) -> rule1)) -> rule3))] @3: Charlie is young.[(((triple5 ((((triple5) -> rule1)) -> rule3)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((((triple1) -> (rule2 % int2)) triple1) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((((triple11) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple9 ((triple11) -> (rule5 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple11) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
((triple8) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple5) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple11) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple10 triple9) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple11) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple11) -> (rule5 % int3)) ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) ((triple8) -> (rule3 % int3))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple5 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3