Anne is blue. Anne is cold. Anne is green. Anne is kind. Anne is nice. Anne is rough. Dave is blue. Dave is cold. Dave is green. Dave is kind. Dave is nice. Fiona is green. Fiona is kind. Fiona is nice. Fiona is rough. All rough things are round. All rough, green things are cold. Kind, blue things are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
All rough, green things are cold.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Kind, blue things are rough.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Dave is kind.
True
1
proof
[(triple10)]
("Dave" "is" "kind" "+")
triple10
Fiona is not nice.
False
1
inv-proof
[(triple14)]
("Fiona" "is" "nice" "-")
triple14
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((triple6 triple3) -> rule2) OR ((((triple4 triple1) -> rule3) triple3) -> rule2))] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is nice.[(triple5)] Anne is rough.[(triple6 OR ((triple4 triple1) -> rule3))] Dave is blue.[(triple7)] Dave is cold.[(triple8 OR ((((triple10 triple7) -> rule3) triple9) -> rule2))] Dave is green.[(triple9)] Dave is kind.[(triple10)] Dave is nice.[(triple11)] Fiona is green.[(triple12)] Fiona is kind.[(triple13)] Fiona is nice.[(triple14)] Fiona is rough.[(triple15)] @1: Anne is round.[(((triple6) -> rule1) OR ((((triple4 triple1) -> rule3)) -> rule1))] Dave is rough.[(((triple10 triple7) -> rule3))] Fiona is cold.[(((triple15 triple12) -> rule2))] Fiona is round.[(((triple15) -> rule1))] @2: Dave is round.[(((((triple10 triple7) -> rule3)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple6 triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4 triple1) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple4 triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((((triple10 triple7) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
triple12
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
Fiona is nice.
("Fiona" "is" "nice" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Anne is round.
("Anne" "is" "round" "+")
((triple6) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple10 triple7) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple15 triple12) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple15) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple10 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2