Gary is blue. Gary is furry. Gary is green. Gary is white. Gary is young. Harry is big. Harry is blue. Harry is furry. Harry is green. Harry is young. All round, young things are big. All furry things are round. If Harry is young then Harry is green. Furry, young things are white. Big things are green. Blue, green things are white.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
All round, young things are big.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Harry is young then Harry is green.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "green" "+"))
Furry, young things are white.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Blue, green things are white.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Gary is not young.
False
1
inv-proof
[(triple5)]
("Gary" "is" "young" "-")
triple5
@0: Gary is blue.[(triple1)] Gary is furry.[(triple2)] Gary is green.[(triple3 OR ((((((triple2) -> rule2) triple5) -> rule1)) -> rule5))] Gary is white.[(triple4 OR ((triple1 triple3) -> rule6) OR ((triple2 triple5) -> rule4) OR ((triple1 ((((((triple2) -> rule2) triple5) -> rule1)) -> rule5)) -> rule6))] Gary is young.[(triple5)] Harry is big.[(triple6 OR ((((triple8) -> rule2) triple10) -> rule1))] Harry is blue.[(triple7)] Harry is furry.[(triple8)] Harry is green.[(triple9 OR ((triple10) -> rule3) OR ((triple6) -> rule5) OR ((((((triple8) -> rule2) triple10) -> rule1)) -> rule5))] Harry is young.[(triple10)] @1: Gary is round.[(((triple2) -> rule2))] Harry is round.[(((triple8) -> rule2))] Harry is white.[(((triple7 triple9) -> rule6) OR ((triple8 triple10) -> rule4) OR ((triple7 ((triple10) -> rule3)) -> rule6) OR ((triple7 ((triple6) -> rule5)) -> rule6) OR ((triple7 ((((((triple8) -> rule2) triple10) -> rule1)) -> rule5)) -> rule6))] @2: Gary is big.[(((((triple2) -> rule2) triple5) -> rule1))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((((((triple2) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple4
((triple1 triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple2 triple5) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple1 ((((((triple2) -> (rule2 % int4)) triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple6) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((((triple8) -> (rule2 % int3)) triple10) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
((triple2) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple8) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple7 triple9) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8 triple10) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple7 ((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple7 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple7 ((((((triple8) -> (rule2 % int4)) triple10) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
((((triple2) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2