Erin is green. Erin is red. Erin is round. Erin is smart. Erin is young. Fiona is cold. Fiona is furry. Fiona is green. Fiona is red. Fiona is round. Fiona is smart. Fiona is young. If Fiona is cold then Fiona is red. Cold, young things are red. Red things are round. Young things are cold. If something is smart and round then it is furry. All cold things are green.
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Fiona is cold then Fiona is red.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
Cold, young things are red.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is smart and round then it is furry.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple2 OR ((((triple5) -> rule4) triple5) -> rule2))]
("Erin" "is" "red" "+")
triple2
((((triple5) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Fiona is not smart.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "smart" "-")
triple11
Erin is furry.
True
3
proof
[(((triple4 triple3) -> rule5) OR ((triple4 ((triple2) -> rule3)) -> rule5) OR ((triple4 ((((((triple5) -> rule4) triple5) -> rule2)) -> rule3)) -> rule5))]
("Erin" "is" "furry" "+")
((triple4 triple3) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple4 ((((((triple5) -> (rule4 % int4)) triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not cold.
False
2
inv-proof
[(((triple5) -> rule4))]
("Erin" "is" "cold" "-")
((triple5) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
@0: Erin is green.[(triple1 OR ((((triple5) -> rule4)) -> rule6))] Erin is red.[(triple2 OR ((((triple5) -> rule4) triple5) -> rule2))] Erin is round.[(triple3 OR ((triple2) -> rule3) OR ((((((triple5) -> rule4) triple5) -> rule2)) -> rule3))] Erin is smart.[(triple4)] Erin is young.[(triple5)] Fiona is cold.[(triple6 OR ((triple12) -> rule4))] Fiona is furry.[(triple7 OR ((triple11 triple10) -> rule5) OR ((triple11 ((triple9) -> rule3)) -> rule5) OR ((triple11 ((((triple6) -> rule1)) -> rule3)) -> rule5) OR ((triple11 ((((triple6 triple12) -> rule2)) -> rule3)) -> rule5) OR ((triple11 ((((((triple12) -> rule4)) -> rule1)) -> rule3)) -> rule5) OR ((triple11 ((((((triple12) -> rule4) triple12) -> rule2)) -> rule3)) -> rule5))] Fiona is green.[(triple8 OR ((triple6) -> rule6) OR ((((triple12) -> rule4)) -> rule6))] Fiona is red.[(triple9 OR ((triple6) -> rule1) OR ((triple6 triple12) -> rule2) OR ((((triple12) -> rule4)) -> rule1) OR ((((triple12) -> rule4) triple12) -> rule2))] Fiona is round.[(triple10 OR ((triple9) -> rule3) OR ((((triple6) -> rule1)) -> rule3) OR ((((triple6 triple12) -> rule2)) -> rule3) OR ((((((triple12) -> rule4)) -> rule1)) -> rule3) OR ((((((triple12) -> rule4) triple12) -> rule2)) -> rule3))] Fiona is smart.[(triple11)] Fiona is young.[(triple12)] @1: Erin is cold.[(((triple5) -> rule4))] Erin is furry.[(((triple4 triple3) -> rule5) OR ((triple4 ((triple2) -> rule3)) -> rule5) OR ((triple4 ((((((triple5) -> rule4) triple5) -> rule2)) -> rule3)) -> rule5))]
Erin is green.
("Erin" "is" "green" "+")
triple1
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple2
((((triple5) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple3
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((((triple5) -> (rule4 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple12) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((triple11 triple10) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple11 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((triple11 ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((triple11 ((((triple6 triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((triple11 ((((((triple12) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
((triple11 ((((((triple12) -> (rule4 % int4)) triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple8
((triple6) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
triple9
((triple6) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple6 triple12) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple12) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple6 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((triple12) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Erin is cold.
("Erin" "is" "cold" "+")
((triple5) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4 triple3) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple4 ((((((triple5) -> (rule4 % int4)) triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4