Anne is kind. Anne is nice. Anne is smart. Gary is big. Gary is blue. Gary is kind. Gary is nice. Gary is red. Gary is rough. Gary is smart. If someone is nice then they are rough. All red people are blue. If someone is rough and nice then they are red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and nice then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Gary is nice.
True
1
proof
[(triple7)]
("Gary" "is" "nice" "+")
triple7
Gary is not big.
False
1
inv-proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Anne is rough.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "rough" "-")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Anne" "is" "red" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Anne" "is" "red" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule2))]
("Anne" "is" "blue" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not blue.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule2))]
("Anne" "is" "blue" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3)] Gary is big.[(triple4)] Gary is blue.[(triple5 OR ((triple8) -> rule2) OR ((((triple9 triple7) -> rule3)) -> rule2) OR ((((((triple7) -> rule1) triple7) -> rule3)) -> rule2))] Gary is kind.[(triple6)] Gary is nice.[(triple7)] Gary is red.[(triple8 OR ((triple9 triple7) -> rule3) OR ((((triple7) -> rule1) triple7) -> rule3))] Gary is rough.[(triple9 OR ((triple7) -> rule1))] Gary is smart.[(triple10)] @1: Anne is rough.[(((triple2) -> rule1))] @2: Anne is red.[(((((triple2) -> rule1) triple2) -> rule3))] @3: Anne is blue.[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
((triple8) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple9 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple7) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
((triple9 triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3