Dave is green. Dave is quiet. Dave is white. Rough, white people are furry. If Dave is red and Dave is nice then Dave is quiet. If someone is rough then they are nice. If someone is quiet and nice then they are red. If someone is green then they are rough. Nice people are quiet. If someone is green then they are rough. If someone is rough and green then they are white.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Rough, white people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Dave is red and Dave is nice then Dave is quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "+"))
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and nice then they are red.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and green then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Dave is quiet.
True
1
proof
[(triple2 OR ((((((triple1) -> rule5)) -> rule3)) -> rule6) OR ((((((triple1) -> rule7)) -> rule3)) -> rule6))]
("Dave" "is" "quiet" "+")
triple2
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule7))]
("Dave" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple1) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule7))]
("Dave" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple1) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule1) OR ((((triple1) -> rule7) triple3) -> rule1) OR ((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule5) ((((triple1) -> rule7) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule7) ((((triple1) -> rule5) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule7) ((((triple1) -> rule7) triple1) -> rule8)) -> rule1))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not nice.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
True
5
proof
[(((triple2 ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((triple2 ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4))]
("Dave" "is" "red" "+")
((triple2 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple2 ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is not red.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((triple2 ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4))]
("Dave" "is" "red" "-")
((triple2 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple2 ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
@0: Dave is green.[(triple1)] Dave is quiet.[(triple2 OR ((((((triple1) -> rule5)) -> rule3)) -> rule6) OR ((((((triple1) -> rule7)) -> rule3)) -> rule6))] Dave is white.[(triple3 OR ((((triple1) -> rule5) triple1) -> rule8) OR ((((triple1) -> rule7) triple1) -> rule8))] @1: Dave is rough.[(((triple1) -> rule5) OR ((triple1) -> rule7))] @2: Dave is furry.[(((((triple1) -> rule5) triple3) -> rule1) OR ((((triple1) -> rule7) triple3) -> rule1) OR ((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule5) ((((triple1) -> rule7) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule7) ((((triple1) -> rule5) triple1) -> rule8)) -> rule1) OR ((((triple1) -> rule7) ((((triple1) -> rule7) triple1) -> rule8)) -> rule1))] Dave is nice.[(((((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule7)) -> rule3))] @3: Dave is red.[(((triple2 ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((triple2 ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule5)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule5)) -> rule3)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule6) ((((triple1) -> rule7)) -> rule3)) -> rule4))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple3
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple1) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple2 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple2 ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4