Dave is blue. Dave is cold. Dave is quiet. If Dave is quiet and Dave is blue then Dave is nice. If something is big then it is white. All blue, furry things are big. All cold things are furry. If something is nice then it is furry. If something is quiet then it is nice. All quiet, white things are blue. Furry, big things are quiet.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If Dave is quiet and Dave is blue then Dave is nice.
((("Dave" "is" "quiet" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "nice" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All blue, furry things are big.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All quiet, white things are blue.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Furry, big things are quiet.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple3 OR ((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8))]
("Dave" "is" "quiet" "+")
triple3
((((triple2) -> (rule4 % int3)) ((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is nice.
True
2
proof
[(((triple3) -> rule6) OR ((triple3 triple1) -> rule1) OR ((((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6) OR ((((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8) triple1) -> rule1))]
("Dave" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple3 triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((((triple2) -> (rule4 % int4)) ((triple1 ((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
((((((triple2) -> (rule4 % int4)) ((triple1 ((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3) -> rule6)) -> rule5) OR ((((triple3 triple1) -> rule1)) -> rule5))]
("Dave" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
True
4
proof
[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "big" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not big.
False
4
inv-proof
[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "big" "-")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
True
5
proof
[(((((triple1 ((triple2) -> rule4)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "white" "+")
((((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((triple1 ((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple1 ((((triple3 triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not white.
False
5
inv-proof
[(((((triple1 ((triple2) -> rule4)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "white" "-")
((((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((triple1 ((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple1 ((((triple3 triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is quiet.[(triple3 OR ((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8))] @1: Dave is furry.[(((triple2) -> rule4) OR ((((triple3) -> rule6)) -> rule5) OR ((((triple3 triple1) -> rule1)) -> rule5))] Dave is nice.[(((triple3) -> rule6) OR ((triple3 triple1) -> rule1) OR ((((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6) OR ((((((triple2) -> rule4) ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule8) triple1) -> rule1))] @2: Dave is big.[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3))] @3: Dave is white.[(((((triple1 ((triple2) -> rule4)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((triple1 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule3)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((((triple2) -> (rule4 % int3)) ((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple3 triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((((triple2) -> (rule4 % int4)) ((triple1 ((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
((((((triple2) -> (rule4 % int4)) ((triple1 ((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((triple1 ((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((triple1 ((((triple3 triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4