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