Anne is blue. Anne is not green. Anne is quiet. Anne is not red. Anne is young. Charlie is blue. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is white. Charlie is young. Red things are white. Young, quiet things are white. If something is white and not red then it is not green. All green things are young. If something is quiet and blue then it is young. All red things are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
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" "+")
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Young, quiet things are white.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is white and not red then it is not green.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "-"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is quiet and blue then it is young.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "blue" "-")
triple6
@0: Anne is blue.[(triple1)] Anne is not green.[(triple2 OR ((((triple5 triple3) -> rule2) triple4) -> rule3) OR ((((((triple3 triple1) -> rule5) triple3) -> rule2) triple4) -> rule3))] Anne is not red.[(triple4)] Anne is quiet.[(triple3)] Anne is young.[(triple5 OR ((triple3 triple1) -> rule5))] Charlie is blue.[(triple6)] Charlie is green.[(triple7)] Charlie is kind.[(triple8)] Charlie is quiet.[(triple9 OR ((triple10) -> rule6))] Charlie is red.[(triple10)] Charlie is white.[(triple11 OR ((triple10) -> rule1) OR ((triple12 triple9) -> rule2) OR ((triple12 ((triple10) -> rule6)) -> rule2) OR ((((triple7) -> rule4) triple9) -> rule2) OR ((((triple9 triple6) -> rule5) triple9) -> rule2) OR ((((triple7) -> rule4) ((triple10) -> rule6)) -> rule2) OR ((((triple9 triple6) -> rule5) ((triple10) -> rule6)) -> rule2) OR ((((((triple10) -> rule6) triple6) -> rule5) triple9) -> rule2) OR ((((((triple10) -> rule6) triple6) -> rule5) ((triple10) -> rule6)) -> rule2))] Charlie is young.[(triple12 OR ((triple7) -> rule4) OR ((triple9 triple6) -> rule5) OR ((((triple10) -> rule6) triple6) -> rule5))] @1: Anne is white.[(((triple5 triple3) -> rule2) OR ((((triple3 triple1) -> rule5) triple3) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple2
((((triple5 triple3) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple3 triple1) -> (rule5 % int3)) triple3) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not red.
("Anne" "is" "red" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple3 triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
((triple10) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is white.
("Charlie" "is" "white" "+")
triple11
((triple10) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple12 triple9) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple12 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple7) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple9 triple6) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple7) -> (rule4 % int3)) ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple9 triple6) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple10) -> (rule6 % int3)) triple6) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple10) -> (rule6 % int3)) triple6) -> (rule5 % int2)) ((triple10) -> (rule6 % int3))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple12
((triple7) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple9 triple6) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple10) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple5 triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3 triple1) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2