Charlie is furry. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is white. Charlie is young. Dave is furry. Dave is quiet. Dave is rough. Dave is smart. Young things are white. If something is furry then it is rough. All smart things are young. If something is rough then it is quiet. If something is smart then it is furry. If something is white and rough then it is round.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is white and rough then it is round.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule1))]
("Charlie" "is" "white" "-")
triple5
((triple6) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is young.
True
2
proof
[(((triple10) -> rule3))]
("Dave" "is" "young" "+")
((triple10) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple10) -> rule3))]
("Dave" "is" "young" "-")
((triple10) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
True
3
proof
[(((((triple10) -> rule3)) -> rule1))]
("Dave" "is" "white" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule1))]
("Dave" "is" "white" "-")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
True
5
proof
[(((((((triple10) -> rule3)) -> rule1) triple9) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((triple7) -> rule2)) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((((triple10) -> rule5)) -> rule2)) -> rule6))]
("Dave" "is" "round" "+")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple10) -> (rule3 % int4))) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((((triple10) -> (rule3 % int5))) -> (rule1 % int4)) ((((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Dave is not round.
False
5
inv-proof
[(((((((triple10) -> rule3)) -> rule1) triple9) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((triple7) -> rule2)) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((((triple10) -> rule5)) -> rule2)) -> rule6))]
("Dave" "is" "round" "-")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple10) -> (rule3 % int4))) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((((triple10) -> (rule3 % int5))) -> (rule1 % int4)) ((((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
@0: Charlie is furry.[(triple1)] Charlie is quiet.[(triple2 OR ((triple3) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] Charlie is rough.[(triple3 OR ((triple1) -> rule2))] Charlie is round.[(triple4 OR ((triple5 triple3) -> rule6) OR ((triple5 ((triple1) -> rule2)) -> rule6) OR ((((triple6) -> rule1) triple3) -> rule6) OR ((((triple6) -> rule1) ((triple1) -> rule2)) -> rule6))] Charlie is white.[(triple5 OR ((triple6) -> rule1))] Charlie is young.[(triple6)] Dave is furry.[(triple7 OR ((triple10) -> rule5))] Dave is quiet.[(triple8 OR ((triple9) -> rule4) OR ((((triple7) -> rule2)) -> rule4) OR ((((((triple10) -> rule5)) -> rule2)) -> rule4))] Dave is rough.[(triple9 OR ((triple7) -> rule2) OR ((((triple10) -> rule5)) -> rule2))] Dave is smart.[(triple10)] @1: Dave is young.[(((triple10) -> rule3))] @2: Dave is white.[(((((triple10) -> rule3)) -> rule1))] @3: Dave is round.[(((((((triple10) -> rule3)) -> rule1) triple9) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((triple7) -> rule2)) -> rule6) OR ((((((triple10) -> rule3)) -> rule1) ((((triple10) -> rule5)) -> rule2)) -> rule6))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((triple3) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple5 triple3) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple6) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple6) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple6) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple10) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple9) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
((triple10) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple10) -> (rule3 % int4))) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((((triple10) -> (rule3 % int5))) -> (rule1 % int4)) ((((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5