Anne is big. Anne is green. Anne is young. If Anne is red then Anne is round. All young, rough people are big. All rough, green people are red. If Anne is green and Anne is big then Anne is young. All red, round people are rough. If someone is young and big then they are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is red then Anne is round.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "round" "+"))
All young, rough people are big.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All rough, green people are red.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Anne is green and Anne is big then Anne is young.
((("Anne" "is" "green" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "young" "+"))
All red, round people are rough.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and big then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple3 OR ((triple2 triple1) -> rule4))]
("Anne" "is" "young" "-")
triple3
((triple2 triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
True
3
proof
[(((triple3 triple1) -> rule6) OR ((((triple2 triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "rough" "+")
((triple3 triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((triple3 triple1) -> rule6) OR ((((triple2 triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "rough" "-")
((triple3 triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
True
5
proof
[(((((triple3 triple1) -> rule6) triple2) -> rule3) OR ((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3))]
("Anne" "is" "red" "+")
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not red.
False
5
inv-proof
[(((((triple3 triple1) -> rule6) triple2) -> rule3) OR ((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3))]
("Anne" "is" "red" "-")
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is round.
True
6
proof
[(((((((triple3 triple1) -> rule6) triple2) -> rule3)) -> rule1) OR ((((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3)) -> rule1))]
("Anne" "is" "round" "+")
((((((triple3 triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is not round.
False
6
inv-proof
[(((((((triple3 triple1) -> rule6) triple2) -> rule3)) -> rule1) OR ((((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3)) -> rule1))]
("Anne" "is" "round" "-")
((((((triple3 triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is young.[(triple3 OR ((triple2 triple1) -> rule4))] @1: Anne is rough.[(((triple3 triple1) -> rule6) OR ((((triple2 triple1) -> rule4) triple1) -> rule6))] @2: Anne is red.[(((((triple3 triple1) -> rule6) triple2) -> rule3) OR ((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3))] @3: Anne is round.[(((((((triple3 triple1) -> rule6) triple2) -> rule3)) -> rule1) OR ((((((((triple2 triple1) -> rule4) triple1) -> rule6) triple2) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple2 triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((triple3 triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4