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