Gary is big. Gary is red. Gary is round. All big things are red. If Gary is white and Gary is red then Gary is big. If something is round and white then it is young. All red things are blue. If something is red and blue then it is young. All big things are young. If something is big then it is quiet. White things are big.
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Gary is white and Gary is red then Gary is big.
((("Gary" "is" "white" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "big" "+"))
If something is round and white then it is young.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is red and blue then it is young.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Gary is red.
True
1
proof
[(triple2 OR ((triple1) -> rule1))]
("Gary" "is" "red" "+")
triple2
((triple1) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not big.
False
1
inv-proof
[(triple1)]
("Gary" "is" "big" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple1) -> rule7))]
("Gary" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple1) -> rule1)) -> rule4))]
("Gary" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
@0: Gary is big.[(triple1)] Gary is red.[(triple2 OR ((triple1) -> rule1))] Gary is round.[(triple3)] @1: Gary is blue.[(((triple2) -> rule4) OR ((((triple1) -> rule1)) -> rule4))] Gary is quiet.[(((triple1) -> rule7))] Gary is young.[(((triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule5) OR ((((triple1) -> rule1) ((triple2) -> rule4)) -> rule5) OR ((triple2 ((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule4)) -> rule5))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
triple2
((triple1) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple1) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3