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