Anne is cold. Anne is rough. Anne is smart. Gary is cold. Gary is nice. Gary is rough. Gary is smart. If Anne is big then Anne is blue. If Gary is big and Gary is rough then Gary is blue. If something is cold then it is big. All cold, blue things are green. If Gary is blue then Gary is green. Smart things are green. Cold things are smart. Green things are big.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Anne is big then Anne is blue.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "blue" "+"))
If Gary is big and Gary is rough then Gary is blue.
((("Gary" "is" "big" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "blue" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All cold, blue things are green.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Gary is blue then Gary is green.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Anne is rough.
True
1
proof
[(triple2)]
("Anne" "is" "rough" "+")
triple2
Gary is not smart.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule7))]
("Gary" "is" "smart" "-")
triple7
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
@0: Anne is cold.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3 OR ((triple1) -> rule7))] Gary is cold.[(triple4)] Gary is nice.[(triple5)] Gary is rough.[(triple6)] Gary is smart.[(triple7 OR ((triple4) -> rule7))] @1: Anne is big.[(((triple1) -> rule3) OR ((((triple3) -> rule6)) -> rule8) OR ((((((triple1) -> rule7)) -> rule6)) -> rule8))] Anne is green.[(((triple3) -> rule6) OR ((((triple1) -> rule7)) -> rule6) OR ((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule4))] Gary is big.[(((triple4) -> rule3) OR ((((triple7) -> rule6)) -> rule8) OR ((((((triple4) -> rule7)) -> rule6)) -> rule8))] Gary is green.[(((triple7) -> rule6) OR ((((triple4) -> rule7)) -> rule6) OR ((((((triple4) -> rule3) triple6) -> rule2)) -> rule5) OR ((triple4 ((((triple4) -> rule3) triple6) -> rule2)) -> rule4))] @2: Anne is blue.[(((((triple1) -> rule3)) -> rule1) OR ((((((triple3) -> rule6)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule7)) -> rule6)) -> rule8)) -> rule1))] Gary is blue.[(((((triple4) -> rule3) triple6) -> rule2) OR ((((((triple7) -> rule6)) -> rule8) triple6) -> rule2) OR ((((((((triple4) -> rule7)) -> rule6)) -> rule8) triple6) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple1) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple4) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple4 ((((triple4) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule8 % int2)) triple6) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((((triple4) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple6) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4