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