Charlie is big. Charlie is furry. Charlie is rough. Charlie is smart. Charlie is white. Charlie is young. Dave is big. Dave is furry. Dave is round. Dave is smart. Dave is white. Dave is young. If Charlie is furry then Charlie is young. If Dave is young and Dave is round then Dave is smart. All round, furry people are smart. If Dave is smart then Dave is young. Big people are rough. White, big people are rough. White people are big. Young people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If Charlie is furry then Charlie is young.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "young" "+"))
If Dave is young and Dave is round then Dave is smart.
((("Dave" "is" "young" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "smart" "+"))
All round, furry people are smart.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart then Dave is young.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "young" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
White, big people are rough.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Dave is young.
True
1
proof
[(triple12 OR ((triple10) -> rule4) OR ((((triple9 triple8) -> rule3)) -> rule4))]
("Dave" "is" "young" "+")
triple12
((triple10) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple9 triple8) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule7))]
("Charlie" "is" "big" "-")
triple1
((triple5) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is rough.
True
2
proof
[(((triple7) -> rule5) OR ((triple11 triple7) -> rule6) OR ((((triple11) -> rule7)) -> rule5) OR ((triple11 ((triple11) -> rule7)) -> rule6))]
("Dave" "is" "rough" "+")
((triple7) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple11 triple7) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple11 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not rough.
False
2
inv-proof
[(((triple7) -> rule5) OR ((triple11 triple7) -> rule6) OR ((((triple11) -> rule7)) -> rule5) OR ((triple11 ((triple11) -> rule7)) -> rule6))]
("Dave" "is" "rough" "-")
((triple7) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple11 triple7) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple11 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
@0: Charlie is big.[(triple1 OR ((triple5) -> rule7))] Charlie is furry.[(triple2)] Charlie is rough.[(triple3 OR ((triple1) -> rule5) OR ((triple5 triple1) -> rule6) OR ((((triple5) -> rule7)) -> rule5) OR ((triple5 ((triple5) -> rule7)) -> rule6))] Charlie is smart.[(triple4 OR ((triple6) -> rule8) OR ((((triple2) -> rule1)) -> rule8))] Charlie is white.[(triple5)] Charlie is young.[(triple6 OR ((triple2) -> rule1))] Dave is big.[(triple7 OR ((triple11) -> rule7))] Dave is furry.[(triple8)] Dave is round.[(triple9)] Dave is smart.[(triple10 OR ((triple12) -> rule8) OR ((triple12 triple9) -> rule2) OR ((triple9 triple8) -> rule3))] Dave is white.[(triple11)] Dave is young.[(triple12 OR ((triple10) -> rule4) OR ((((triple9 triple8) -> rule3)) -> rule4))] @1: Dave is rough.[(((triple7) -> rule5) OR ((triple11 triple7) -> rule6) OR ((((triple11) -> rule7)) -> rule5) OR ((triple11 ((triple11) -> rule7)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple5) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple6) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple7
((triple11) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
((triple12) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple12 triple9) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple9 triple8) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
((triple10) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple9 triple8) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple7) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple11 triple7) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple11 ((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2