Dave is big. Dave is green. Dave is nice. Dave is rough. Dave is round. Dave is smart. Dave is young. All nice people are rough. If Dave is young then Dave is green. If someone is smart then they are round. If Dave is smart and Dave is big then Dave is round. Round, nice people are green. All rough people are big. If someone is young and round then they are green. If someone is big and green then they are round.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Dave is young then Dave is green.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "green" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart and Dave is big then Dave is round.
((("Dave" "is" "smart" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "round" "+"))
Round, nice people are green.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is young and round then they are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is big and green then they are round.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Dave is smart.
True
1
proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
Dave is not young.
False
1
inv-proof
[(triple7)]
("Dave" "is" "young" "-")
triple7
@0: Dave is big.[(triple1 OR ((triple4) -> rule6) OR ((((triple3) -> rule1)) -> rule6))] Dave is green.[(triple2 OR ((triple7) -> rule2) OR ((triple5 triple3) -> rule5) OR ((triple7 triple5) -> rule7) OR ((triple7 ((triple6) -> rule3)) -> rule7) OR ((triple7 ((triple6 triple1) -> rule4)) -> rule7) OR ((((triple6) -> rule3) triple3) -> rule5) OR ((((triple6 triple1) -> rule4) triple3) -> rule5) OR ((triple7 ((triple6 ((triple4) -> rule6)) -> rule4)) -> rule7) OR ((((triple6 ((triple4) -> rule6)) -> rule4) triple3) -> rule5) OR ((triple7 ((triple6 ((((triple3) -> rule1)) -> rule6)) -> rule4)) -> rule7) OR ((((triple6 ((((triple3) -> rule1)) -> rule6)) -> rule4) triple3) -> rule5))] Dave is nice.[(triple3)] Dave is rough.[(triple4 OR ((triple3) -> rule1))] Dave is round.[(triple5 OR ((triple6) -> rule3) OR ((triple1 triple2) -> rule8) OR ((triple6 triple1) -> rule4) OR ((triple1 ((triple7) -> rule2)) -> rule8) OR ((triple6 ((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple2) -> rule8) OR ((((triple4) -> rule6) ((triple7) -> rule2)) -> rule8) OR ((triple6 ((((triple3) -> rule1)) -> rule6)) -> rule4) OR ((((((triple3) -> rule1)) -> rule6) triple2) -> rule8) OR ((((((triple3) -> rule1)) -> rule6) ((triple7) -> rule2)) -> rule8))] Dave is smart.[(triple6)] Dave is young.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5 triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple7 triple5) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple7 ((triple6) -> (rule3 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple7 ((triple6 triple1) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6 triple1) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple7 ((triple6 ((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((triple6 ((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple7 ((triple6 ((((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple6 ((((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6 triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple6 ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4) -> (rule6 % int3)) ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple6 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple3) -> (rule1 % int4))) -> (rule6 % int3)) ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7