Anne is blue. Anne is green. Anne is kind. Anne is quiet. Anne is rough. Anne is round. Anne is white. All quiet things are white. Rough things are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Anne is white.
True
1
proof
[(triple7 OR ((triple4) -> rule1) OR ((((triple5) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
triple7
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not kind.
False
1
inv-proof
[(triple3)]
("Anne" "is" "kind" "-")
triple3
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is quiet.[(triple4 OR ((triple5) -> rule2))] Anne is rough.[(triple5)] Anne is round.[(triple6)] Anne is white.[(triple7 OR ((triple4) -> rule1) OR ((((triple5) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple5) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2