Anne is big. Anne is nice. Anne is quiet. Anne is round. Anne is smart. Anne is white. Anne is young. If something is young then it is quiet. If something is white then it is big. If something is big then it is nice. If something is round and smart then it is big. If Anne is smart then Anne is quiet. Quiet, round things are white. All smart, white things are round. If Anne is nice and Anne is smart then Anne is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is round and smart then it is big.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If Anne is smart then Anne is quiet.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "quiet" "+"))
Quiet, round things are white.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All smart, white things are round.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If Anne is nice and Anne is smart then Anne is young.
((("Anne" "is" "nice" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
Anne is quiet.
True
1
proof
[(triple3 OR ((triple5) -> rule5) OR ((triple7) -> rule1) OR ((((triple2 triple5) -> rule8)) -> rule1) OR ((((((triple1) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((triple6) -> rule2)) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((triple4 triple5) -> rule4)) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((((triple5 triple6) -> rule7) triple5) -> rule4)) -> rule3) triple5) -> rule8)) -> rule1))]
("Anne" "is" "quiet" "+")
triple3
((triple5) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple7) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((((triple1) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((triple4 triple5) -> (rule4 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((((triple5 triple6) -> (rule7 % int5)) triple5) -> (rule4 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not nice.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule3) OR ((((triple6) -> rule2)) -> rule3) OR ((((triple4 triple5) -> rule4)) -> rule3) OR ((((((triple3 triple4) -> rule6)) -> rule2)) -> rule3) OR ((((((triple5 triple6) -> rule7) triple5) -> rule4)) -> rule3) OR ((((((((triple5) -> rule5) triple4) -> rule6)) -> rule2)) -> rule3) OR ((((((((triple7) -> rule1) triple4) -> rule6)) -> rule2)) -> rule3))]
("Anne" "is" "nice" "-")
triple2
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple3 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((triple5 triple6) -> (rule7 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((((triple5) -> (rule5 % int4)) triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
@0: Anne is big.[(triple1 OR ((triple6) -> rule2) OR ((triple4 triple5) -> rule4) OR ((((triple3 triple4) -> rule6)) -> rule2) OR ((((triple5 triple6) -> rule7) triple5) -> rule4) OR ((((((triple5) -> rule5) triple4) -> rule6)) -> rule2) OR ((((((triple7) -> rule1) triple4) -> rule6)) -> rule2) OR ((((((((triple2 triple5) -> rule8)) -> rule1) triple4) -> rule6)) -> rule2))] Anne is nice.[(triple2 OR ((triple1) -> rule3) OR ((((triple6) -> rule2)) -> rule3) OR ((((triple4 triple5) -> rule4)) -> rule3) OR ((((((triple3 triple4) -> rule6)) -> rule2)) -> rule3) OR ((((((triple5 triple6) -> rule7) triple5) -> rule4)) -> rule3) OR ((((((((triple5) -> rule5) triple4) -> rule6)) -> rule2)) -> rule3) OR ((((((((triple7) -> rule1) triple4) -> rule6)) -> rule2)) -> rule3))] Anne is quiet.[(triple3 OR ((triple5) -> rule5) OR ((triple7) -> rule1) OR ((((triple2 triple5) -> rule8)) -> rule1) OR ((((((triple1) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((triple6) -> rule2)) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((triple4 triple5) -> rule4)) -> rule3) triple5) -> rule8)) -> rule1) OR ((((((((((triple5 triple6) -> rule7) triple5) -> rule4)) -> rule3) triple5) -> rule8)) -> rule1))] Anne is round.[(triple4 OR ((triple5 triple6) -> rule7))] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple3 triple4) -> rule6) OR ((((triple5) -> rule5) triple4) -> rule6) OR ((((triple7) -> rule1) triple4) -> rule6) OR ((((((triple2 triple5) -> rule8)) -> rule1) triple4) -> rule6) OR ((((((((triple1) -> rule3) triple5) -> rule8)) -> rule1) triple4) -> rule6) OR ((((((((((triple4 triple5) -> rule4)) -> rule3) triple5) -> rule8)) -> rule1) triple4) -> rule6))] Anne is young.[(triple7 OR ((triple2 triple5) -> rule8) OR ((((triple1) -> rule3) triple5) -> rule8) OR ((((((triple6) -> rule2)) -> rule3) triple5) -> rule8) OR ((((((triple4 triple5) -> rule4)) -> rule3) triple5) -> rule8) OR ((((((((triple3 triple4) -> rule6)) -> rule2)) -> rule3) triple5) -> rule8) OR ((((((((triple5 triple6) -> rule7) triple5) -> rule4)) -> rule3) triple5) -> rule8) OR ((((((((((triple5) -> rule5) triple4) -> rule6)) -> rule2)) -> rule3) triple5) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple5 triple6) -> (rule7 % int2)) triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple5) -> (rule5 % int3)) triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((triple7) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((((triple2 triple5) -> (rule8 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple3 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((triple5 triple6) -> (rule7 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((((triple5) -> (rule5 % int4)) triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple5) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple7) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2 triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((((triple1) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((triple4 triple5) -> (rule4 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((((triple5 triple6) -> (rule7 % int5)) triple5) -> (rule4 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple5 triple6) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple3 triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple7) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple2 triple5) -> (rule8 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((((triple1) -> (rule3 % int4)) triple5) -> (rule8 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((((((((triple4 triple5) -> (rule4 % int5))) -> (rule3 % int4)) triple5) -> (rule8 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple2 triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple4 triple5) -> (rule4 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((((triple3 triple4) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((((((triple5 triple6) -> (rule7 % int4)) triple5) -> (rule4 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((((((((triple5) -> (rule5 % int5)) triple4) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5