Anne is big. Anne is red. Anne is rough. If someone is white and red then they are blue. If someone is red then they are white. White, red people are young. All white, rough people are big. All big, red people are young. If Anne is young and Anne is rough then Anne is white. Green, rough people are big. Blue, red people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
If someone is white and red then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
White, red people are young.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
All white, rough people are big.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All big, red people are young.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Anne is young and Anne is rough then Anne is white.
((("Anne" "is" "young" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "white" "+"))
Green, rough people are big.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Blue, red people are green.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Anne is not big.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule2) triple3) -> rule4) OR ((((((((triple2) -> rule2) triple2) -> rule1) triple2) -> rule8) triple3) -> rule7))]
("Anne" "is" "big" "-")
triple1
((((triple2) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((((triple2) -> (rule2 % int4)) triple2) -> (rule1 % int3)) triple2) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is white.
True
2
proof
[(((triple2) -> rule2) OR ((((triple1 triple2) -> rule5) triple3) -> rule6))]
("Anne" "is" "white" "+")
((triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1 triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule5) OR ((((triple2) -> rule2) triple2) -> rule3) OR ((((((triple2) -> rule2) triple3) -> rule4) triple2) -> rule5) OR ((((((((((triple2) -> rule2) triple2) -> rule1) triple2) -> rule8) triple3) -> rule7) triple2) -> rule5))]
("Anne" "is" "young" "-")
((triple1 triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple2) -> (rule2 % int3)) triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((((triple2) -> (rule2 % int5)) triple2) -> (rule1 % int4)) triple2) -> (rule8 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
@0: Anne is big.[(triple1 OR ((((triple2) -> rule2) triple3) -> rule4) OR ((((((((triple2) -> rule2) triple2) -> rule1) triple2) -> rule8) triple3) -> rule7))] Anne is red.[(triple2)] Anne is rough.[(triple3)] @1: Anne is white.[(((triple2) -> rule2) OR ((((triple1 triple2) -> rule5) triple3) -> rule6))] Anne is young.[(((triple1 triple2) -> rule5) OR ((((triple2) -> rule2) triple2) -> rule3) OR ((((((triple2) -> rule2) triple3) -> rule4) triple2) -> rule5) OR ((((((((((triple2) -> rule2) triple2) -> rule1) triple2) -> rule8) triple3) -> rule7) triple2) -> rule5))] @2: Anne is blue.[(((((triple2) -> rule2) triple2) -> rule1) OR ((((((triple1 triple2) -> rule5) triple3) -> rule6) triple2) -> rule1))] @3: Anne is green.[(((((((triple2) -> rule2) triple2) -> rule1) triple2) -> rule8) OR ((((((((triple1 triple2) -> rule5) triple3) -> rule6) triple2) -> rule1) triple2) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((triple2) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((((triple2) -> (rule2 % int4)) triple2) -> (rule1 % int3)) triple2) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1 triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple2) -> (rule2 % int3)) triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((((triple2) -> (rule2 % int5)) triple2) -> (rule1 % int4)) triple2) -> (rule8 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple1 triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple1 triple2) -> (rule5 % int4)) triple3) -> (rule6 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4