Anne is big. Anne is blue. Anne is nice. Anne is white. Anne is young. Fiona is big. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is round. Fiona is white. Fiona is young. If Anne is quiet and Anne is nice then Anne is round. If something is blue then it is young. If something is nice and young then it is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Anne is quiet and Anne is nice then Anne is round.
((("Anne" "is" "quiet" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "round" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is nice and young then it is round.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Anne is young.
True
1
proof
[(triple5 OR ((triple2) -> rule2))]
("Anne" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is not young.
False
1
inv-proof
[(triple12 OR ((triple7) -> rule2))]
("Fiona" "is" "young" "-")
triple12
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is round.
True
3
proof
[(((triple3 triple5) -> rule3) OR ((triple3 ((triple2) -> rule2)) -> rule3))]
("Anne" "is" "round" "+")
((triple3 triple5) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not round.
False
3
inv-proof
[(((triple3 triple5) -> rule3) OR ((triple3 ((triple2) -> rule2)) -> rule3))]
("Anne" "is" "round" "-")
((triple3 triple5) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is nice.[(triple3)] Anne is white.[(triple4)] Anne is young.[(triple5 OR ((triple2) -> rule2))] Fiona is big.[(triple6)] Fiona is blue.[(triple7)] Fiona is nice.[(triple8)] Fiona is quiet.[(triple9)] Fiona is round.[(triple10 OR ((triple8 triple12) -> rule3) OR ((triple8 ((triple7) -> rule2)) -> rule3))] Fiona is white.[(triple11)] Fiona is young.[(triple12 OR ((triple7) -> rule2))] @1: Anne is round.[(((triple3 triple5) -> rule3) OR ((triple3 ((triple2) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple8 triple12) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple8 ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple5) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2