Erin is blue. Erin is red. Erin is rough. Erin is round. Fiona is blue. Fiona is furry. Fiona is red. Fiona is rough. Fiona is round. Gary is big. Gary is blue. Gary is furry. Gary is red. Gary is rough. Gary is round. Blue things are big. Blue, furry things are round. If Gary is blue and Gary is furry then Gary is rough. If Erin is big then Erin is cold. Round things are blue. Red, rough things are cold. If something is rough then it is big. All rough, big things are blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Blue, furry things are round.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Gary is blue and Gary is furry then Gary is rough.
((("Gary" "is" "blue" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
If Erin is big then Erin is cold.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "cold" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Red, rough things are cold.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All rough, big things are blue.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Fiona is blue.
True
1
proof
[(triple5 OR ((triple9) -> rule5) OR ((triple8 ((triple8) -> rule7)) -> rule8))]
("Fiona" "is" "blue" "+")
triple5
((triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple8 ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not furry.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "furry" "-")
triple6
@0: Erin is blue.[(triple1 OR ((triple4) -> rule5) OR ((triple3 ((triple3) -> rule7)) -> rule8))] Erin is red.[(triple2)] Erin is rough.[(triple3)] Erin is round.[(triple4)] Fiona is blue.[(triple5 OR ((triple9) -> rule5) OR ((triple8 ((triple8) -> rule7)) -> rule8))] Fiona is furry.[(triple6)] Fiona is red.[(triple7)] Fiona is rough.[(triple8)] Fiona is round.[(triple9 OR ((triple5 triple6) -> rule2) OR ((((triple8 ((triple8) -> rule7)) -> rule8) triple6) -> rule2))] Gary is big.[(triple10 OR ((triple11) -> rule1) OR ((triple14) -> rule7) OR ((((triple15) -> rule5)) -> rule1) OR ((((triple11 triple12) -> rule3)) -> rule7) OR ((((((triple15) -> rule5) triple12) -> rule3)) -> rule7))] Gary is blue.[(triple11 OR ((triple15) -> rule5) OR ((triple14 triple10) -> rule8) OR ((triple14 ((triple14) -> rule7)) -> rule8))] Gary is furry.[(triple12)] Gary is red.[(triple13)] Gary is rough.[(triple14 OR ((triple11 triple12) -> rule3) OR ((((triple15) -> rule5) triple12) -> rule3))] Gary is round.[(triple15 OR ((triple11 triple12) -> rule2) OR ((((triple14 triple10) -> rule8) triple12) -> rule2) OR ((((triple14 ((triple14) -> rule7)) -> rule8) triple12) -> rule2))] @1: Erin is big.[(((triple1) -> rule1) OR ((triple3) -> rule7) OR ((((triple4) -> rule5)) -> rule1))] Erin is cold.[(((triple2 triple3) -> rule6) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple3) -> rule7)) -> rule4) OR ((((((triple4) -> rule5)) -> rule1)) -> rule4))] Fiona is big.[(((triple5) -> rule1) OR ((triple8) -> rule7) OR ((((triple9) -> rule5)) -> rule1))] Fiona is cold.[(((triple7 triple8) -> rule6))] Gary is cold.[(((triple13 triple14) -> rule6) OR ((triple13 ((triple11 triple12) -> rule3)) -> rule6) OR ((triple13 ((((triple15) -> rule5) triple12) -> rule3)) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple4) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple3 ((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple8 ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
((triple5 triple6) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple8 ((triple8) -> (rule7 % int3))) -> (rule8 % int2)) triple6) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple11) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple14) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple15) -> (rule5 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple11 triple12) -> (rule3 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple15) -> (rule5 % int3)) triple12) -> (rule3 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple11
((triple15) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple14 triple10) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple14 ((triple14) -> (rule7 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple11 triple12) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple15) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple15
((triple11 triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14 triple10) -> (rule8 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple14 ((triple14) -> (rule7 % int3))) -> (rule8 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple2 triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((triple5) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple8) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7 triple8) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple13 triple14) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple13 ((triple11 triple12) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple13 ((((triple15) -> (rule5 % int3)) triple12) -> (rule3 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3