Anne is big. Anne is green. Anne is nice. Anne is rough. Anne is round. Bob is big. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is rough. Bob is round. Erin is green. Erin is nice. Erin is rough. Erin is round. All nice things are green. All nice things are furry. All kind, furry things are big. All kind, big things are furry. Rough things are kind. All green things are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All kind, furry things are big.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All kind, big things are furry.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Anne is round.
True
1
proof
[(triple5)]
("Anne" "is" "round" "+")
triple5
Anne is not green.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule1))]
("Anne" "is" "green" "-")
triple2
((triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
True
2
proof
[(((triple4) -> rule5))]
("Anne" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple4) -> rule5))]
("Anne" "is" "kind" "-")
((triple4) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is big.
True
5
proof
[(((((triple15) -> rule5) ((triple13) -> rule6)) -> rule3) OR ((((triple15) -> rule5) ((triple14) -> rule2)) -> rule3) OR ((((triple15) -> rule5) ((((triple14) -> rule1)) -> rule6)) -> rule3))]
("Erin" "is" "big" "+")
((((triple15) -> (rule5 % int3)) ((triple13) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int3)) ((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not big.
False
5
inv-proof
[(((((triple15) -> rule5) ((triple13) -> rule6)) -> rule3) OR ((((triple15) -> rule5) ((triple14) -> rule2)) -> rule3) OR ((((triple15) -> rule5) ((((triple14) -> rule1)) -> rule6)) -> rule3))]
("Erin" "is" "big" "-")
((((triple15) -> (rule5 % int3)) ((triple13) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int3)) ((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
@0: Anne is big.[(triple1 OR ((((triple4) -> rule5) ((triple2) -> rule6)) -> rule3) OR ((((triple4) -> rule5) ((triple3) -> rule2)) -> rule3) OR ((((triple4) -> rule5) ((((triple3) -> rule1)) -> rule6)) -> rule3))] Anne is green.[(triple2 OR ((triple3) -> rule1))] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5)] Bob is big.[(triple6 OR ((triple9 triple7) -> rule3) OR ((triple9 ((triple10) -> rule2)) -> rule3) OR ((triple9 ((triple8) -> rule6)) -> rule3) OR ((((triple11) -> rule5) triple7) -> rule3) OR ((((triple11) -> rule5) ((triple10) -> rule2)) -> rule3) OR ((((triple11) -> rule5) ((triple8) -> rule6)) -> rule3) OR ((triple9 ((((triple10) -> rule1)) -> rule6)) -> rule3) OR ((((triple11) -> rule5) ((((triple10) -> rule1)) -> rule6)) -> rule3))] Bob is furry.[(triple7 OR ((triple10) -> rule2) OR ((triple8) -> rule6) OR ((triple9 triple6) -> rule4) OR ((((triple10) -> rule1)) -> rule6) OR ((((triple11) -> rule5) triple6) -> rule4))] Bob is green.[(triple8 OR ((triple10) -> rule1))] Bob is kind.[(triple9 OR ((triple11) -> rule5))] Bob is nice.[(triple10)] Bob is rough.[(triple11)] Bob is round.[(triple12)] Erin is green.[(triple13 OR ((triple14) -> rule1))] Erin is nice.[(triple14)] Erin is rough.[(triple15)] Erin is round.[(triple16)] @1: Anne is furry.[(((triple2) -> rule6) OR ((triple3) -> rule2) OR ((((triple3) -> rule1)) -> rule6) OR ((((triple4) -> rule5) triple1) -> rule4))] Anne is kind.[(((triple4) -> rule5))] Erin is furry.[(((triple13) -> rule6) OR ((triple14) -> rule2) OR ((((triple14) -> rule1)) -> rule6))] Erin is kind.[(((triple15) -> rule5))] @2: Erin is big.[(((((triple15) -> rule5) ((triple13) -> rule6)) -> rule3) OR ((((triple15) -> rule5) ((triple14) -> rule2)) -> rule3) OR ((((triple15) -> rule5) ((((triple14) -> rule1)) -> rule6)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((triple4) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple4) -> (rule5 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple4) -> (rule5 % int4)) ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
((triple9 triple7) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple9 ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple9 ((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple11) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple11) -> (rule5 % int3)) ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple11) -> (rule5 % int3)) ((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple11) -> (rule5 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
triple7
((triple10) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple8) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple9 triple6) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple11) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple8
((triple10) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple9
((triple11) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
triple11
Bob is round.
("Bob" "is" "round" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
((triple14) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple14
Erin is rough.
("Erin" "is" "rough" "+")
triple15
Erin is round.
("Erin" "is" "round" "+")
triple16
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple3) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple13) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple14) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple15) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple15) -> (rule5 % int3)) ((triple13) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int3)) ((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple15) -> (rule5 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4