Anne is furry. Anne is green. Anne is nice. Anne is rough. Anne is round. Anne is white. Anne is young. Charlie is furry. Charlie is green. Charlie is rough. Charlie is round. Charlie is white. Charlie is young. Dave is furry. Dave is green. Dave is nice. If Dave is round then Dave is rough. All round, green people are rough. If someone is rough then they are white. All nice, young people are round. Young, green people are white. Furry people are young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
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 green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
If Dave is round then Dave is rough.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "rough" "+"))
All round, green people are rough.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All nice, young people are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Young, green people are white.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Dave is furry.
True
1
proof
[(triple14)]
("Dave" "is" "furry" "+")
triple14
Charlie is not rough.
False
1
inv-proof
[(triple10 OR ((triple11 triple9) -> rule2))]
("Charlie" "is" "rough" "-")
triple10
((triple11 triple9) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is young.
True
2
proof
[(((triple14) -> rule6))]
("Dave" "is" "young" "+")
((triple14) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple14) -> rule6))]
("Dave" "is" "young" "-")
((triple14) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
True
4
proof
[(((triple16 ((triple14) -> rule6)) -> rule4))]
("Dave" "is" "round" "+")
((triple16 ((triple14) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not round.
False
4
inv-proof
[(((triple16 ((triple14) -> rule6)) -> rule4))]
("Dave" "is" "round" "-")
((triple16 ((triple14) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
True
5
proof
[(((((triple16 ((triple14) -> rule6)) -> rule4)) -> rule1) OR ((((triple16 ((triple14) -> rule6)) -> rule4) triple15) -> rule2))]
("Dave" "is" "rough" "+")
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2)) triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not rough.
False
5
inv-proof
[(((((triple16 ((triple14) -> rule6)) -> rule4)) -> rule1) OR ((((triple16 ((triple14) -> rule6)) -> rule4) triple15) -> rule2))]
("Dave" "is" "rough" "-")
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2)) triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4 OR ((triple5 triple2) -> rule2) OR ((((triple3 triple7) -> rule4) triple2) -> rule2) OR ((((triple3 ((triple1) -> rule6)) -> rule4) triple2) -> rule2))] Anne is round.[(triple5 OR ((triple3 triple7) -> rule4) OR ((triple3 ((triple1) -> rule6)) -> rule4))] Anne is white.[(triple6 OR ((triple4) -> rule3) OR ((triple7 triple2) -> rule5) OR ((((triple5 triple2) -> rule2)) -> rule3) OR ((((triple1) -> rule6) triple2) -> rule5) OR ((((((triple3 triple7) -> rule4) triple2) -> rule2)) -> rule3) OR ((((((triple3 ((triple1) -> rule6)) -> rule4) triple2) -> rule2)) -> rule3))] Anne is young.[(triple7 OR ((triple1) -> rule6))] Charlie is furry.[(triple8)] Charlie is green.[(triple9)] Charlie is rough.[(triple10 OR ((triple11 triple9) -> rule2))] Charlie is round.[(triple11)] Charlie is white.[(triple12 OR ((triple10) -> rule3) OR ((triple13 triple9) -> rule5) OR ((((triple11 triple9) -> rule2)) -> rule3) OR ((((triple8) -> rule6) triple9) -> rule5))] Charlie is young.[(triple13 OR ((triple8) -> rule6))] Dave is furry.[(triple14)] Dave is green.[(triple15)] Dave is nice.[(triple16)] @1: Dave is young.[(((triple14) -> rule6))] @2: Dave is round.[(((triple16 ((triple14) -> rule6)) -> rule4))] Dave is white.[(((((triple14) -> rule6) triple15) -> rule5) OR ((((((triple16 ((triple14) -> rule6)) -> rule4)) -> rule1)) -> rule3) OR ((((((triple16 ((triple14) -> rule6)) -> rule4) triple15) -> rule2)) -> rule3))] @3: Dave is rough.[(((((triple16 ((triple14) -> rule6)) -> rule4)) -> rule1) OR ((((triple16 ((triple14) -> rule6)) -> rule4) triple15) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple5 triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple3 triple7) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple3 ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple3 triple7) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple7 triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((((triple3 triple7) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple3 ((triple1) -> (rule6 % int4))) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
((triple11 triple9) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple10) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple13 triple9) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple11 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple8) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple13
((triple8) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple14
Dave is green.
("Dave" "is" "green" "+")
triple15
Dave is nice.
("Dave" "is" "nice" "+")
triple16
Dave is young.
("Dave" "is" "young" "+")
((triple14) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple16 ((triple14) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple14) -> (rule6 % int2)) triple15) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple16 ((triple14) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((((triple16 ((triple14) -> (rule6 % int4))) -> (rule4 % int3)) triple15) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple16 ((triple14) -> (rule6 % int3))) -> (rule4 % int2)) triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3