Anne is red. Anne is white. Harry is cold. Harry is furry. Harry is red. Harry is rough. Harry is smart. All red people are smart. If Anne is smart then Anne is green. All green people are rough. All cold people are furry. All green people are white. If Harry is red then Harry is green. If Anne is furry then Anne is white. If someone is rough then they are cold.
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Anne is smart then Anne is green.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "green" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Harry is red then Harry is green.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "green" "+"))
If Anne is furry then Anne is white.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "white" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule4) OR ((((triple6) -> rule8)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule3)) -> rule8)) -> rule4))]
("Harry" "is" "furry" "-")
triple4
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
@0: Anne is red.[(triple1)] Anne is white.[(triple2 OR ((((((triple1) -> rule1)) -> rule2)) -> rule5) OR ((((((((((((triple1) -> rule1)) -> rule2)) -> rule3)) -> rule8)) -> rule4)) -> rule7))] Harry is cold.[(triple3 OR ((triple6) -> rule8) OR ((((((triple5) -> rule6)) -> rule3)) -> rule8))] Harry is furry.[(triple4 OR ((triple3) -> rule4) OR ((((triple6) -> rule8)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule3)) -> rule8)) -> rule4))] Harry is red.[(triple5)] Harry is rough.[(triple6 OR ((((triple5) -> rule6)) -> rule3))] Harry is smart.[(triple7 OR ((triple5) -> rule1))] @1: Anne is smart.[(((triple1) -> rule1))] Harry is green.[(((triple5) -> rule6))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule2))] Harry is white.[(((((triple5) -> rule6)) -> rule5))] @3: Anne is rough.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))] @4: Anne is cold.[(((((((((triple1) -> rule1)) -> rule2)) -> rule3)) -> rule8))] @5: Anne is furry.[(((((((((((triple1) -> rule1)) -> rule2)) -> rule3)) -> rule8)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((((((((triple1) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is smart.
("Anne" "is" "smart" "+")
int6
Harry is cold.
("Harry" "is" "cold" "+")
triple3
((triple6) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((((triple5) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple5) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple5) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5