Dave is green. Dave is red. Dave is smart. Harry is furry. Harry is green. Harry is nice. Harry is smart. If something is red then it is furry. All rough things are quiet. All smart things are rough. If something is smart and furry then it is quiet. All quiet, furry things are green. If something is rough and green then it is smart. If something is nice then it is furry. All green, furry things are nice.
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is smart and furry then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All quiet, furry things are green.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is rough and green then it is smart.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All green, furry things are nice.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Harry is furry.
True
1
proof
[(triple4 OR ((triple6) -> rule7))]
("Harry" "is" "furry" "+")
triple4
((triple6) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not green.
False
1
inv-proof
[(triple5 OR ((((triple7 triple4) -> rule4) triple4) -> rule5) OR ((((triple7 triple4) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple7) -> rule3)) -> rule2) triple4) -> rule5) OR ((((triple7 ((triple6) -> rule7)) -> rule4) triple4) -> rule5) OR ((((((triple7) -> rule3)) -> rule2) ((triple6) -> rule7)) -> rule5) OR ((((triple7 ((triple6) -> rule7)) -> rule4) ((triple6) -> rule7)) -> rule5))]
("Harry" "is" "green" "-")
triple5
((((triple7 triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7 triple4) -> (rule4 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple7 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple7) -> (rule3 % int4))) -> (rule2 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((triple7 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Dave is furry.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple3) -> rule3)) -> rule2) OR ((triple3 ((triple2) -> rule1)) -> rule4))]
("Dave" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple3 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2) OR ((triple3 ((triple2) -> rule1)) -> rule4))]
("Dave" "is" "quiet" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple3 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
@0: Dave is green.[(triple1 OR ((((((triple3) -> rule3)) -> rule2) ((triple2) -> rule1)) -> rule5) OR ((((triple3 ((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule5))] Dave is red.[(triple2)] Dave is smart.[(triple3)] Harry is furry.[(triple4 OR ((triple6) -> rule7))] Harry is green.[(triple5 OR ((((triple7 triple4) -> rule4) triple4) -> rule5) OR ((((triple7 triple4) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple7) -> rule3)) -> rule2) triple4) -> rule5) OR ((((triple7 ((triple6) -> rule7)) -> rule4) triple4) -> rule5) OR ((((((triple7) -> rule3)) -> rule2) ((triple6) -> rule7)) -> rule5) OR ((((triple7 ((triple6) -> rule7)) -> rule4) ((triple6) -> rule7)) -> rule5))] Harry is nice.[(triple6 OR ((triple5 triple4) -> rule8) OR ((((((triple7 triple4) -> rule4) triple4) -> rule5) triple4) -> rule8) OR ((((((((triple7) -> rule3)) -> rule2) triple4) -> rule5) triple4) -> rule8))] Harry is smart.[(triple7)] @1: Dave is furry.[(((triple2) -> rule1))] Dave is rough.[(((triple3) -> rule3))] Harry is quiet.[(((triple7 triple4) -> rule4) OR ((((triple7) -> rule3)) -> rule2) OR ((triple7 ((triple6) -> rule7)) -> rule4))] Harry is rough.[(((triple7) -> rule3))] @2: Dave is nice.[(((triple1 ((triple2) -> rule1)) -> rule8) OR ((((((((triple3) -> rule3)) -> rule2) ((triple2) -> rule1)) -> rule5) ((triple2) -> rule1)) -> rule8) OR ((((((triple3 ((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule5) ((triple2) -> rule1)) -> rule8))] Dave is quiet.[(((((triple3) -> rule3)) -> rule2) OR ((triple3 ((triple2) -> rule1)) -> rule4))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((((((triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple3 ((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((triple6) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple5
((((triple7 triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7 triple4) -> (rule4 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple7 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple7) -> (rule3 % int4))) -> (rule2 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((triple7 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple6
((triple5 triple4) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((((triple7 triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule2 % int3)) triple4) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple7 ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((((triple3) -> (rule3 % int5))) -> (rule2 % int4)) ((triple2) -> (rule1 % int3))) -> (rule5 % int2)) ((triple2) -> (rule1 % int3))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple3 ((triple2) -> (rule1 % int4))) -> (rule4 % int3)) ((triple2) -> (rule1 % int4))) -> (rule5 % int2)) ((triple2) -> (rule1 % int4))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple3 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2