Anne is blue. Anne is cold. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is white. Harry is blue. Harry is cold. Harry is nice. Harry is red. Harry is rough. Harry is round. Harry is white. Rough, nice things are blue. Round things are blue. All white things are red. If something is nice then it is cold. If Harry is rough then Harry is round. If something is round and white then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Rough, nice things are blue.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Harry is rough then Harry is round.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
If something is round and white then it is nice.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple7) -> rule3))]
("Anne" "is" "red" "+")
triple4
((triple7) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple13 OR ((triple12) -> rule5))]
("Harry" "is" "round" "-")
triple13
((triple12) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
@0: Anne is blue.[(triple1 OR ((triple6) -> rule2) OR ((triple5 triple3) -> rule1) OR ((triple5 ((triple6 triple7) -> rule6)) -> rule1))] Anne is cold.[(triple2 OR ((triple3) -> rule4) OR ((((triple6 triple7) -> rule6)) -> rule4))] Anne is nice.[(triple3 OR ((triple6 triple7) -> rule6))] Anne is red.[(triple4 OR ((triple7) -> rule3))] Anne is rough.[(triple5)] Anne is round.[(triple6)] Anne is white.[(triple7)] Harry is blue.[(triple8 OR ((triple13) -> rule2) OR ((triple12 triple10) -> rule1) OR ((((triple12) -> rule5)) -> rule2) OR ((triple12 ((triple13 triple14) -> rule6)) -> rule1) OR ((triple12 ((((triple12) -> rule5) triple14) -> rule6)) -> rule1))] Harry is cold.[(triple9 OR ((triple10) -> rule4) OR ((((triple13 triple14) -> rule6)) -> rule4) OR ((((((triple12) -> rule5) triple14) -> rule6)) -> rule4))] Harry is nice.[(triple10 OR ((triple13 triple14) -> rule6) OR ((((triple12) -> rule5) triple14) -> rule6))] Harry is red.[(triple11 OR ((triple14) -> rule3))] Harry is rough.[(triple12)] Harry is round.[(triple13 OR ((triple12) -> rule5))] Harry is white.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple6) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple5 triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple5 ((triple6 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple3) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple6 triple7) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple7) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple13) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12 triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple12 ((triple13 triple14) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple12 ((((triple12) -> (rule5 % int3)) triple14) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple10) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple13 triple14) -> (rule6 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple12) -> (rule5 % int3)) triple14) -> (rule6 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple13 triple14) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple12) -> (rule5 % int2)) triple14) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple14) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple12) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14