Fiona is blue. Fiona is green. Fiona is nice. Fiona is smart. Fiona is white. Gary is blue. Gary is cold. Gary is green. Gary is nice. Gary is quiet. Gary is smart. Gary is white. If Fiona is white and Fiona is nice then Fiona is smart. All quiet people are cold. Green, blue people are quiet. All cold, smart people are blue. All cold people are smart. Nice people are smart.
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Fiona is white and Fiona is nice then Fiona is smart.
((("Fiona" "is" "white" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "smart" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Green, blue people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All cold, smart people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Gary is green.
True
1
proof
[(triple8)]
("Gary" "is" "green" "+")
triple8
Fiona is not smart.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule6) OR ((triple5 triple3) -> rule1) OR ((((((triple2 triple1) -> rule3)) -> rule2)) -> rule5))]
("Fiona" "is" "smart" "-")
triple4
((triple3) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple2 triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
@0: Fiona is blue.[(triple1)] Fiona is green.[(triple2)] Fiona is nice.[(triple3)] Fiona is smart.[(triple4 OR ((triple3) -> rule6) OR ((triple5 triple3) -> rule1) OR ((((((triple2 triple1) -> rule3)) -> rule2)) -> rule5))] Fiona is white.[(triple5)] Gary is blue.[(triple6 OR ((triple7 triple11) -> rule4) OR ((triple7 ((triple7) -> rule5)) -> rule4) OR ((triple7 ((triple9) -> rule6)) -> rule4) OR ((((triple10) -> rule2) triple11) -> rule4) OR ((((triple10) -> rule2) ((triple7) -> rule5)) -> rule4) OR ((((triple10) -> rule2) ((triple9) -> rule6)) -> rule4) OR ((triple7 ((((triple10) -> rule2)) -> rule5)) -> rule4) OR ((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule5)) -> rule4))] Gary is cold.[(triple7 OR ((triple10) -> rule2) OR ((((triple8 triple6) -> rule3)) -> rule2))] Gary is green.[(triple8)] Gary is nice.[(triple9)] Gary is quiet.[(triple10 OR ((triple8 triple6) -> rule3) OR ((triple8 ((triple7 triple11) -> rule4)) -> rule3) OR ((triple8 ((triple7 ((triple7) -> rule5)) -> rule4)) -> rule3) OR ((triple8 ((triple7 ((triple9) -> rule6)) -> rule4)) -> rule3))] Gary is smart.[(triple11 OR ((triple7) -> rule5) OR ((triple9) -> rule6) OR ((((triple10) -> rule2)) -> rule5) OR ((((((triple8 triple6) -> rule3)) -> rule2)) -> rule5))] Gary is white.[(triple12)] @1: Fiona is quiet.[(((triple2 triple1) -> rule3))] @2: Fiona is cold.[(((((triple2 triple1) -> rule3)) -> rule2))]
Fiona is blue.
("Fiona" "is" "blue" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
((triple3) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple2 triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
((triple7 triple11) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple7 ((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple10) -> (rule2 % int2)) triple11) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple10) -> (rule2 % int3)) ((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple10) -> (rule2 % int3)) ((((triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple10) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple8 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
((triple8 triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple8 ((triple7 triple11) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple8 ((triple7 ((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple8 ((triple7 ((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple11
((triple7) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple9) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple8 triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple12
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple2 triple1) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2