Erin is cold. Erin is kind. Erin is round. Erin is white. Erin is young. Harry is cold. Harry is furry. Harry is nice. Harry is round. Harry is young. If something is nice and furry then it is kind. Round, cold things are furry. If Harry is nice then Harry is young. If something is round and young then it is cold. All cold, kind things are white. If Harry is round then Harry is white.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is nice and furry then it is kind.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Round, cold things are furry.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If Harry is nice then Harry is young.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "young" "+"))
If something is round and young then it is cold.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All cold, kind things are white.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Harry is round then Harry is white.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule3))]
("Harry" "is" "young" "-")
triple10
((triple8) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
True
3
proof
[(((triple8 triple7) -> rule1) OR ((triple8 ((triple9 triple6) -> rule2)) -> rule1) OR ((triple8 ((triple9 ((triple9 triple10) -> rule4)) -> rule2)) -> rule1) OR ((triple8 ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "kind" "+")
((triple8 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple9 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple8 ((triple9 ((triple9 triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple8 ((triple9 ((triple9 ((triple8) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Erin is not furry.
False
3
inv-proof
[(((triple3 triple1) -> rule2) OR ((triple3 ((triple3 triple5) -> rule4)) -> rule2))]
("Erin" "is" "furry" "-")
((triple3 triple1) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple3 ((triple3 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
@0: Erin is cold.[(triple1 OR ((triple3 triple5) -> rule4))] Erin is kind.[(triple2)] Erin is round.[(triple3)] Erin is white.[(triple4 OR ((triple1 triple2) -> rule5) OR ((((triple3 triple5) -> rule4) triple2) -> rule5))] Erin is young.[(triple5)] Harry is cold.[(triple6 OR ((triple9 triple10) -> rule4) OR ((triple9 ((triple8) -> rule3)) -> rule4))] Harry is furry.[(triple7 OR ((triple9 triple6) -> rule2) OR ((triple9 ((triple9 triple10) -> rule4)) -> rule2) OR ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2))] Harry is nice.[(triple8)] Harry is round.[(triple9)] Harry is young.[(triple10 OR ((triple8) -> rule3))] @1: Erin is furry.[(((triple3 triple1) -> rule2) OR ((triple3 ((triple3 triple5) -> rule4)) -> rule2))] Harry is kind.[(((triple8 triple7) -> rule1) OR ((triple8 ((triple9 triple6) -> rule2)) -> rule1) OR ((triple8 ((triple9 ((triple9 triple10) -> rule4)) -> rule2)) -> rule1) OR ((triple8 ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2)) -> rule1))] Harry is white.[(((triple9) -> rule6) OR ((triple6 ((triple8 triple7) -> rule1)) -> rule5) OR ((((triple9 triple10) -> rule4) ((triple8 triple7) -> rule1)) -> rule5) OR ((triple6 ((triple8 ((triple9 triple6) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 triple10) -> rule4) ((triple8 ((triple9 triple6) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 ((triple8) -> rule3)) -> rule4) ((triple8 triple7) -> rule1)) -> rule5) OR ((((triple9 ((triple8) -> rule3)) -> rule4) ((triple8 ((triple9 triple6) -> rule2)) -> rule1)) -> rule5) OR ((triple6 ((triple8 ((triple9 ((triple9 triple10) -> rule4)) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 triple10) -> rule4) ((triple8 ((triple9 ((triple9 triple10) -> rule4)) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 ((triple8) -> rule3)) -> rule4) ((triple8 ((triple9 ((triple9 triple10) -> rule4)) -> rule2)) -> rule1)) -> rule5) OR ((triple6 ((triple8 ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 triple10) -> rule4) ((triple8 ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2)) -> rule1)) -> rule5) OR ((((triple9 ((triple8) -> rule3)) -> rule4) ((triple8 ((triple9 ((triple9 ((triple8) -> rule3)) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple3 triple5) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
((triple1 triple2) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3 triple5) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((triple9 triple10) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple9 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple9 triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple9 ((triple9 triple10) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple9 ((triple9 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
((triple8) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple3 triple1) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple3 ((triple3 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple8 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple9 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple8 ((triple9 ((triple9 triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple8 ((triple9 ((triple9 ((triple8) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((triple9) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple6 ((triple8 triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple9 triple10) -> (rule4 % int3)) ((triple8 triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple6 ((triple8 ((triple9 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple9 triple10) -> (rule4 % int4)) ((triple8 ((triple9 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((triple9 ((triple8) -> (rule3 % int4))) -> (rule4 % int3)) ((triple8 triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((((triple9 ((triple8) -> (rule3 % int5))) -> (rule4 % int4)) ((triple8 ((triple9 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
((triple6 ((triple8 ((triple9 ((triple9 triple10) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((triple9 triple10) -> (rule4 % int4)) ((triple8 ((triple9 ((triple9 triple10) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((triple9 ((triple8) -> (rule3 % int5))) -> (rule4 % int4)) ((triple8 ((triple9 ((triple9 triple10) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
((triple6 ((triple8 ((triple9 ((triple9 ((triple8) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
((((triple9 triple10) -> (rule4 % int5)) ((triple8 ((triple9 ((triple9 ((triple8) -> (rule3 % int4))) -> (rule4 % int5))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((triple9 ((triple8) -> (rule3 % int5))) -> (rule4 % int4)) ((triple8 ((triple9 ((triple9 ((triple8) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5