Charlie is not big. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is white. Charlie is young. Dave is big. Dave is green. Dave is kind. Dave is quiet. Dave is not red. Dave is not white. Dave is young. If something is white and not green then it is big. Red things are young. If Dave is kind then Dave is young. Red things are kind. If something is red and not big then it is kind. If something is green and not young then it is quiet. All kind, red things are quiet. If something is big and not young then it is not quiet.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not white.
("Dave" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
If something is white and not green then it is big.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Dave is kind then Dave is young.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "young" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is red and not big then it is kind.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
If something is green and not young then it is quiet.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "quiet" "+"))
All kind, red things are quiet.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is big and not young then it is not quiet.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "quiet" "-"))
Charlie is red.
True
1
proof
[(triple5)]
("Charlie" "is" "red" "+")
triple5
Dave is not green.
False
1
inv-proof
[(triple9)]
("Dave" "is" "green" "-")
triple9
@0: Charlie is green.[(triple2)] Charlie is kind.[(triple3 OR ((triple5) -> rule4) OR ((triple5 triple1) -> rule5))] Charlie is not big.[(triple1)] Charlie is quiet.[(triple4 OR ((triple3 triple5) -> rule7) OR ((((triple5) -> rule4) triple5) -> rule7) OR ((((triple5 triple1) -> rule5) triple5) -> rule7))] Charlie is red.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple5) -> rule2))] Dave is big.[(triple8)] Dave is green.[(triple9)] Dave is kind.[(triple10)] Dave is not red.[(triple12)] Dave is not white.[(triple13)] Dave is quiet.[(triple11)] Dave is young.[(triple14 OR ((triple10) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple5) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple5 triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple3 triple5) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule5 % int2)) triple5) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple5) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is not red.
("Dave" "is" "red" "-")
triple12
Dave is not white.
("Dave" "is" "white" "-")
triple13
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple14
((triple10) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1