Gary is big. Gary is quiet. Gary is white. If something is white then it is nice. All big, nice things are blue. Quiet things are white. If something is blue then it is red. If something is furry then it is blue. Furry things are blue.
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All big, nice things are blue.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple2)]
("Gary" "is" "quiet" "-")
triple2
Gary is nice.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Gary" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
True
4
proof
[(((triple1 ((triple3) -> rule1)) -> rule2) OR ((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "blue" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((triple1 ((triple3) -> rule1)) -> rule2) OR ((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "blue" "-")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
True
5
proof
[(((((triple1 ((triple3) -> rule1)) -> rule2)) -> rule4) OR ((((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "red" "+")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is not red.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule1)) -> rule2)) -> rule4) OR ((((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "red" "-")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
@0: Gary is big.[(triple1)] Gary is quiet.[(triple2)] Gary is white.[(triple3 OR ((triple2) -> rule3))] @1: Gary is nice.[(((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] @2: Gary is blue.[(((triple1 ((triple3) -> rule1)) -> rule2) OR ((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2))] @3: Gary is red.[(((((triple1 ((triple3) -> rule1)) -> rule2)) -> rule4) OR ((((triple1 ((((triple2) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
((triple2) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple1 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((triple1 ((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4