Anne is big. Anne is blue. Anne is green. Anne is rough. Anne is round. Anne is young. Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. Charlie is rough. Charlie is young. Gary is blue. Gary is rough. Gary is round. If someone is blue and big then they are young. If someone is blue and rough then they are big. If someone is young and blue then they are round. If Anne is round then Anne is furry. All big, furry people are rough. If someone is blue then they are green. Round people are young. All round, green people are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is blue and big then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and rough then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is young and blue then they are round.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Anne is round then Anne is furry.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "furry" "+"))
All big, furry people are rough.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All round, green people are rough.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Charlie is furry.
True
1
proof
[(triple9)]
("Charlie" "is" "furry" "+")
triple9
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple2 triple4) -> rule2) OR ((triple2 ((triple5 triple3) -> rule8)) -> rule2) OR ((triple2 ((triple5 ((triple2) -> rule6)) -> rule8)) -> rule2) OR ((triple2 ((((triple6 triple2) -> rule3) triple3) -> rule8)) -> rule2) OR ((triple2 ((((triple6 triple2) -> rule3) ((triple2) -> rule6)) -> rule8)) -> rule2))]
("Anne" "is" "big" "-")
triple1
((triple2 triple4) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple2 ((triple5 triple3) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple2 ((triple5 ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((triple2 ((((triple6 triple2) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple2 ((((triple6 triple2) -> (rule3 % int4)) ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Gary is young.
True
2
proof
[(((triple15) -> rule7) OR ((triple13 ((triple13 triple14) -> rule2)) -> rule1) OR ((triple13 ((triple13 ((triple15 ((triple13) -> rule6)) -> rule8)) -> rule2)) -> rule1))]
("Gary" "is" "young" "+")
((triple15) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple13 ((triple13 triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple13 ((triple13 ((triple15 ((triple13) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Charlie is not round.
False
3
inv-proof
[(((triple12 triple8) -> rule3) OR ((((triple8 triple7) -> rule1) triple8) -> rule3) OR ((((triple8 ((triple8 triple11) -> rule2)) -> rule1) triple8) -> rule3))]
("Charlie" "is" "round" "-")
((triple12 triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple8 triple7) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple8 ((triple8 triple11) -> (rule2 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
@0: Anne is big.[(triple1 OR ((triple2 triple4) -> rule2) OR ((triple2 ((triple5 triple3) -> rule8)) -> rule2) OR ((triple2 ((triple5 ((triple2) -> rule6)) -> rule8)) -> rule2) OR ((triple2 ((((triple6 triple2) -> rule3) triple3) -> rule8)) -> rule2) OR ((triple2 ((((triple6 triple2) -> rule3) ((triple2) -> rule6)) -> rule8)) -> rule2))] Anne is blue.[(triple2)] Anne is green.[(triple3 OR ((triple2) -> rule6))] Anne is rough.[(triple4 OR ((triple5 triple3) -> rule8) OR ((triple1 ((triple5) -> rule4)) -> rule5) OR ((triple5 ((triple2) -> rule6)) -> rule8) OR ((((triple6 triple2) -> rule3) triple3) -> rule8) OR ((((triple6 triple2) -> rule3) ((triple2) -> rule6)) -> rule8) OR ((triple1 ((((triple6 triple2) -> rule3)) -> rule4)) -> rule5) OR ((((((triple2 triple1) -> rule1) triple2) -> rule3) triple3) -> rule8) OR ((((((triple2 triple1) -> rule1) triple2) -> rule3) ((triple2) -> rule6)) -> rule8) OR ((triple1 ((((((triple2 triple1) -> rule1) triple2) -> rule3)) -> rule4)) -> rule5))] Anne is round.[(triple5 OR ((triple6 triple2) -> rule3) OR ((((triple2 triple1) -> rule1) triple2) -> rule3) OR ((((triple2 ((triple2 triple4) -> rule2)) -> rule1) triple2) -> rule3))] Anne is young.[(triple6 OR ((triple5) -> rule7) OR ((triple2 triple1) -> rule1) OR ((triple2 ((triple2 triple4) -> rule2)) -> rule1) OR ((triple2 ((triple2 ((triple5 triple3) -> rule8)) -> rule2)) -> rule1) OR ((triple2 ((triple2 ((triple5 ((triple2) -> rule6)) -> rule8)) -> rule2)) -> rule1))] Charlie is big.[(triple7 OR ((triple8 triple11) -> rule2) OR ((triple8 ((((triple12 triple8) -> rule3) triple10) -> rule8)) -> rule2) OR ((triple8 ((((triple12 triple8) -> rule3) ((triple8) -> rule6)) -> rule8)) -> rule2))] Charlie is blue.[(triple8)] Charlie is furry.[(triple9)] Charlie is green.[(triple10 OR ((triple8) -> rule6))] Charlie is rough.[(triple11 OR ((triple7 triple9) -> rule5) OR ((((triple12 triple8) -> rule3) triple10) -> rule8) OR ((((triple12 triple8) -> rule3) ((triple8) -> rule6)) -> rule8) OR ((((((triple8 triple7) -> rule1) triple8) -> rule3) triple10) -> rule8) OR ((((((triple8 triple7) -> rule1) triple8) -> rule3) ((triple8) -> rule6)) -> rule8))] Charlie is young.[(triple12 OR ((triple8 triple7) -> rule1) OR ((triple8 ((triple8 triple11) -> rule2)) -> rule1))] Gary is blue.[(triple13)] Gary is rough.[(triple14 OR ((triple15 ((triple13) -> rule6)) -> rule8))] Gary is round.[(triple15 OR ((((triple13 ((triple13 triple14) -> rule2)) -> rule1) triple13) -> rule3))] @1: Anne is furry.[(((triple5) -> rule4) OR ((((triple6 triple2) -> rule3)) -> rule4) OR ((((((triple2 triple1) -> rule1) triple2) -> rule3)) -> rule4) OR ((((((triple2 ((triple2 triple4) -> rule2)) -> rule1) triple2) -> rule3)) -> rule4))] Charlie is round.[(((triple12 triple8) -> rule3) OR ((((triple8 triple7) -> rule1) triple8) -> rule3) OR ((((triple8 ((triple8 triple11) -> rule2)) -> rule1) triple8) -> rule3))] Gary is big.[(((triple13 triple14) -> rule2) OR ((triple13 ((triple15 ((triple13) -> rule6)) -> rule8)) -> rule2))] Gary is green.[(((triple13) -> rule6))] Gary is young.[(((triple15) -> rule7) OR ((triple13 ((triple13 triple14) -> rule2)) -> rule1) OR ((triple13 ((triple13 ((triple15 ((triple13) -> rule6)) -> rule8)) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple4) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple2 ((triple5 triple3) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple2 ((triple5 ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((triple2 ((((triple6 triple2) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple2 ((((triple6 triple2) -> (rule3 % int4)) ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple5 triple3) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple5 ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple6 triple2) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple6 triple2) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple1 ((((triple6 triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple2 triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple2 triple1) -> (rule1 % int4)) triple2) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((triple1 ((((((triple2 triple1) -> (rule1 % int4)) triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple6 triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2 triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple2 ((triple2 triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple5) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple2 triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple2 ((triple2 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple2 ((triple2 ((triple5 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple2 ((triple2 ((triple5 ((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
triple7
((triple8 triple11) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple8 ((((triple12 triple8) -> (rule3 % int3)) triple10) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple8 ((((triple12 triple8) -> (rule3 % int4)) ((triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
((triple8) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
((triple7 triple9) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple12 triple8) -> (rule3 % int2)) triple10) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple12 triple8) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple8 triple7) -> (rule1 % int3)) triple8) -> (rule3 % int2)) triple10) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple8 triple7) -> (rule1 % int4)) triple8) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
triple12
((triple8 triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple8 ((triple8 triple11) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple15 ((triple13) -> (rule6 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple15
((((triple13 ((triple13 triple14) -> (rule2 % int3))) -> (rule1 % int2)) triple13) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple6 triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple2 triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple2 ((triple2 triple4) -> (rule2 % int4))) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
((triple12 triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple8 triple7) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple8 ((triple8 triple11) -> (rule2 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple13 triple14) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple13 ((triple15 ((triple13) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple13) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple15) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple13 ((triple13 triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple13 ((triple13 ((triple15 ((triple13) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4