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