Dave is furry. Dave is green. Dave is rough. Dave is round. Dave is white. Harry is furry. Harry is green. Harry is quiet. Harry is rough. Harry is round. Harry is smart. Harry is white. If someone is round then they are smart. Green people are quiet. If someone is white and smart then they are rough. Round, quiet people are green. If Harry is round then Harry is white. All white, green people are round.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and smart then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Round, quiet people are green.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Harry is round then Harry is white.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
All white, green people are round.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple3 OR ((triple5 ((triple4) -> rule1)) -> rule3) OR ((triple5 ((((triple5 triple2) -> rule6)) -> rule1)) -> rule3))]
("Dave" "is" "rough" "+")
triple3
((triple5 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple5 ((((triple5 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Dave is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple5 triple2) -> rule6)) -> rule1))]
("Dave" "is" "smart" "-")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple5 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
@0: Dave is furry.[(triple1)] Dave is green.[(triple2)] Dave is rough.[(triple3 OR ((triple5 ((triple4) -> rule1)) -> rule3) OR ((triple5 ((((triple5 triple2) -> rule6)) -> rule1)) -> rule3))] Dave is round.[(triple4 OR ((triple5 triple2) -> rule6))] Dave is white.[(triple5)] Harry is furry.[(triple6)] Harry is green.[(triple7 OR ((triple10 triple8) -> rule4))] Harry is quiet.[(triple8 OR ((triple7) -> rule2))] Harry is rough.[(triple9 OR ((triple12 triple11) -> rule3) OR ((triple12 ((triple10) -> rule1)) -> rule3) OR ((((triple10) -> rule5) triple11) -> rule3) OR ((((triple10) -> rule5) ((triple10) -> rule1)) -> rule3) OR ((triple12 ((((triple12 triple7) -> rule6)) -> rule1)) -> rule3) OR ((((triple10) -> rule5) ((((triple12 triple7) -> rule6)) -> rule1)) -> rule3))] Harry is round.[(triple10 OR ((triple12 triple7) -> rule6))] Harry is smart.[(triple11 OR ((triple10) -> rule1) OR ((((triple12 triple7) -> rule6)) -> rule1))] Harry is white.[(triple12 OR ((triple10) -> rule5))] @1: Dave is quiet.[(((triple2) -> rule2))] Dave is smart.[(((triple4) -> rule1) OR ((((triple5 triple2) -> rule6)) -> rule1))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
((triple5 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple5 ((((triple5 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple5 triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple10 triple8) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
((triple7) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple12 triple11) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple12 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10) -> (rule5 % int2)) triple11) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple10) -> (rule5 % int3)) ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple12 ((((triple12 triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple10) -> (rule5 % int4)) ((((triple12 triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple12 triple7) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple10) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple5 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2