Charlie is big. Charlie is furry. Charlie is green. Charlie is young. Erin is big. Erin is cold. Erin is furry. Erin is green. Erin is rough. Erin is young. Gary is big. Gary is cold. Gary is furry. Gary is green. Gary is rough. Gary is smart. If Gary is green then Gary is young. If Erin is rough then Erin is green. All green, big things are cold. If Charlie is furry and Charlie is smart then Charlie is young. If something is furry then it is smart. All furry things are cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Gary is green then Gary is young.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "young" "+"))
If Erin is rough then Erin is green.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "green" "+"))
All green, big things are cold.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Charlie is furry and Charlie is smart then Charlie is young.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "young" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Gary is big.
True
1
proof
[(triple11)]
("Gary" "is" "big" "+")
triple11
Erin is not green.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule2))]
("Erin" "is" "green" "-")
triple8
((triple9) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is young.[(triple4 OR ((triple2 ((triple2) -> rule5)) -> rule4))] Erin is big.[(triple5)] Erin is cold.[(triple6 OR ((triple7) -> rule6) OR ((triple8 triple5) -> rule3) OR ((((triple9) -> rule2) triple5) -> rule3))] Erin is furry.[(triple7)] Erin is green.[(triple8 OR ((triple9) -> rule2))] Erin is rough.[(triple9)] Erin is young.[(triple10)] Gary is big.[(triple11)] Gary is cold.[(triple12 OR ((triple13) -> rule6) OR ((triple14 triple11) -> rule3))] Gary is furry.[(triple13)] Gary is green.[(triple14)] Gary is rough.[(triple15)] Gary is smart.[(triple16 OR ((triple13) -> rule5))] @1: Charlie is cold.[(((triple2) -> rule6) OR ((triple3 triple1) -> rule3))] Charlie is smart.[(((triple2) -> rule5))] Erin is smart.[(((triple7) -> rule5))] Gary is young.[(((triple14) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple7) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple8 triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple9) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
((triple9) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple13) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple14 triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16
((triple13) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple14) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1