Harry is big. Harry is cold. Harry is green. Harry is nice. Harry is not red. Harry is round. Harry is white. Nice things are cold. If something is green then it is cold. If something is nice and white then it is green. Cold, big things are white. All round things are white. If something is round and not big then it is nice. If Harry is white and Harry is not green then Harry is red. If Harry is big and Harry is white then Harry is not red.
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is nice and white then it is green.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Cold, big things are white.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is round and not big then it is nice.
((("something" "is" "round" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
If Harry is white and Harry is not green then Harry is red.
((("Harry" "is" "white" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "red" "+"))
If Harry is big and Harry is white then Harry is not red.
((("Harry" "is" "big" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "red" "-"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is red.
False
1
inv-proof
[(triple5 OR ((triple1 triple7) -> rule8) OR ((triple1 ((triple6) -> rule5)) -> rule8) OR ((triple1 ((triple2 triple1) -> rule4)) -> rule8) OR ((triple1 ((((triple3) -> rule2) triple1) -> rule4)) -> rule8) OR ((triple1 ((((triple4) -> rule1) triple1) -> rule4)) -> rule8))]
("Harry" "is" "red" "+")
triple5
((triple1 triple7) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
((triple1 ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple1 ((triple2 triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple1 ((((triple3) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple1 ((((triple4) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
@0: Harry is big.[(triple1)] Harry is cold.[(triple2 OR ((triple3) -> rule2) OR ((triple4) -> rule1) OR ((((triple4 triple7) -> rule3)) -> rule2) OR ((((triple4 ((triple6) -> rule5)) -> rule3)) -> rule2))] Harry is green.[(triple3 OR ((triple4 triple7) -> rule3) OR ((triple4 ((triple6) -> rule5)) -> rule3) OR ((triple4 ((triple2 triple1) -> rule4)) -> rule3) OR ((triple4 ((((triple4) -> rule1) triple1) -> rule4)) -> rule3))] Harry is nice.[(triple4)] Harry is not red.[(triple5 OR ((triple1 triple7) -> rule8) OR ((triple1 ((triple6) -> rule5)) -> rule8) OR ((triple1 ((triple2 triple1) -> rule4)) -> rule8) OR ((triple1 ((((triple3) -> rule2) triple1) -> rule4)) -> rule8) OR ((triple1 ((((triple4) -> rule1) triple1) -> rule4)) -> rule8))] Harry is round.[(triple6)] Harry is white.[(triple7 OR ((triple6) -> rule5) OR ((triple2 triple1) -> rule4) OR ((((triple3) -> rule2) triple1) -> rule4) OR ((((triple4) -> rule1) triple1) -> rule4))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
((triple3) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple4) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple4 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple4 ((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple3
((triple4 triple7) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple4 ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple4 ((triple2 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple4 ((((triple4) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is not red.
("Harry" "is" "red" "-")
triple5
((triple1 triple7) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
((triple1 ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple1 ((triple2 triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple1 ((((triple3) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple1 ((((triple4) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
((triple6) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple2 triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2