Erin is blue. Erin is furry. Erin is quiet. Kind, quiet things are green. All red, kind things are quiet. All quiet things are blue. Green, blue things are furry. If something is round then it is quiet. All green things are red. All blue things are furry. If Erin is furry then Erin is kind.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Kind, quiet things are green.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All red, kind things are quiet.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Green, blue things are furry.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Erin is furry then Erin is kind.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "kind" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Erin is not furry.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule7) OR ((((triple3) -> rule3)) -> rule7))]
("Erin" "is" "furry" "-")
triple2
((triple1) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
True
2
proof
[(((triple2) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((((triple3) -> rule3)) -> rule7)) -> rule8))]
("Erin" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not kind.
False
2
inv-proof
[(((triple2) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((((triple3) -> rule3)) -> rule7)) -> rule8))]
("Erin" "is" "kind" "-")
((triple2) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is green.
True
4
proof
[(((((triple2) -> rule8) triple3) -> rule1) OR ((((((triple1) -> rule7)) -> rule8) triple3) -> rule1) OR ((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1))]
("Erin" "is" "green" "+")
((((triple2) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is not green.
False
4
inv-proof
[(((((triple2) -> rule8) triple3) -> rule1) OR ((((((triple1) -> rule7)) -> rule8) triple3) -> rule1) OR ((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1))]
("Erin" "is" "green" "-")
((((triple2) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is red.
True
5
proof
[(((((((triple2) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6))]
("Erin" "is" "red" "+")
((((((triple2) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is not red.
False
5
inv-proof
[(((((((triple2) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6))]
("Erin" "is" "red" "-")
((((((triple2) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
@0: Erin is blue.[(triple1 OR ((triple3) -> rule3))] Erin is furry.[(triple2 OR ((triple1) -> rule7) OR ((((triple3) -> rule3)) -> rule7))] Erin is quiet.[(triple3)] @1: Erin is kind.[(((triple2) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((((triple3) -> rule3)) -> rule7)) -> rule8))] @2: Erin is green.[(((((triple2) -> rule8) triple3) -> rule1) OR ((((((triple1) -> rule7)) -> rule8) triple3) -> rule1) OR ((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1))] @3: Erin is red.[(((((((triple2) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6) OR ((((((((((triple3) -> rule3)) -> rule7)) -> rule8) triple3) -> rule1)) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple1) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((triple2) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((((((triple2) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5