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