Dave is big. Dave is blue. Dave is green. Dave is not red. Dave is rough. Dave is round. Dave is young. If Dave is green then Dave is not red. If Dave is not young and Dave is not rough then Dave is not blue. If Dave is rough and Dave is red then Dave is blue. If Dave is rough then Dave is blue. All round things are big. If Dave is green then Dave is round. If something is red and big then it is not blue. If something is round and not red then it is blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is green then Dave is not red.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "red" "-"))
If Dave is not young and Dave is not rough then Dave is not blue.
((("Dave" "is" "young" "~") ("Dave" "is" "rough" "~")) -> ("Dave" "is" "blue" "-"))
If Dave is rough and Dave is red then Dave is blue.
((("Dave" "is" "rough" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "blue" "+"))
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Dave is green then Dave is round.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "round" "+"))
If something is red and big then it is not blue.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something is round and not red then it is blue.
((("something" "is" "round" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
Dave is young.
True
1
proof
[(triple7)]
("Dave" "is" "young" "+")
triple7
Dave is red.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule1))]
("Dave" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
@0: Dave is big.[(triple1 OR ((triple6) -> rule5) OR ((((triple3) -> rule6)) -> rule5))] Dave is blue.[(triple2 OR ((triple5) -> rule4) OR ((triple6 triple4) -> rule8) OR ((triple6 ((triple3) -> rule1)) -> rule8) OR ((((triple3) -> rule6) triple4) -> rule8) OR ((((triple3) -> rule6) ((triple3) -> rule1)) -> rule8))] Dave is green.[(triple3)] Dave is not red.[(triple4 OR ((triple3) -> rule1))] Dave is rough.[(triple5)] Dave is round.[(triple6 OR ((triple3) -> rule6))] Dave is young.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple6) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple5) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 triple4) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
((((triple3) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is not red.
("Dave" "is" "red" "-")
triple4
((triple3) -> (rule1 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
((triple3) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7