Dave is big. Dave is furry. Dave is kind. All rough, round people are white. All white people are big. Kind people are round. If someone is rough and kind then they are red. If Dave is round then Dave is rough. If someone is furry then they are kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
All rough, round people are white.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and kind then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Dave is round then Dave is rough.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "rough" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple1 OR ((((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1)) -> rule2) OR ((((((((triple3) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1)) -> rule2) OR ((((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1)) -> rule2) OR ((((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "big" "-")
triple1
((((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple3) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule3 % int5))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Dave is round.
True
2
proof
[(((triple3) -> rule3) OR ((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "round" "+")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not round.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "round" "-")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
True
3
proof
[(((((triple3) -> rule3)) -> rule5) OR ((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Dave" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not rough.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5) OR ((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Dave" "is" "rough" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is red.
True
5
proof
[(((((((triple3) -> rule3)) -> rule5) triple3) -> rule4) OR ((((((triple3) -> rule3)) -> rule5) ((triple2) -> rule6)) -> rule4) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) triple3) -> rule4) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple2) -> rule6)) -> rule4))]
("Dave" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule6 % int4))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not white.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1) OR ((((((triple3) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1))]
("Dave" "is" "white" "-")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int2))) -> (rule3 % int4))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
@0: Dave is big.[(triple1 OR ((((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1)) -> rule2) OR ((((((((triple3) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1)) -> rule2) OR ((((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1)) -> rule2) OR ((((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1)) -> rule2))] Dave is furry.[(triple2)] Dave is kind.[(triple3 OR ((triple2) -> rule6))] @1: Dave is round.[(((triple3) -> rule3) OR ((((triple2) -> rule6)) -> rule3))] @2: Dave is rough.[(((((triple3) -> rule3)) -> rule5) OR ((((((triple2) -> rule6)) -> rule3)) -> rule5))] @3: Dave is red.[(((((((triple3) -> rule3)) -> rule5) triple3) -> rule4) OR ((((((triple3) -> rule3)) -> rule5) ((triple2) -> rule6)) -> rule4) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) triple3) -> rule4) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple2) -> rule6)) -> rule4))] Dave is white.[(((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1) OR ((((((triple3) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule3)) -> rule5) ((((triple2) -> rule6)) -> rule3)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple3) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule3 % int5))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
((((((((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule6 % int4))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule6 % int2))) -> (rule3 % int4))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4