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