Anne is red. Anne is rough. Anne is not round. Anne is not white. Charlie is cold. Charlie is green. Charlie is kind. Charlie is not red. Charlie is rough. Charlie is not round. Charlie is white. Dave is cold. Dave is red. Dave is not rough. Dave is not round. Dave is white. All kind, round things are red. White, kind things are cold. If something is green and rough then it is cold. Red, kind things are cold. All rough things are kind. All green things are kind. White things are green. If something is cold and not white then it is green.
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not round.
("Anne" "is" "round" "-")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is not round.
("Dave" "is" "round" "-")
Dave is white.
("Dave" "is" "white" "+")
All kind, round things are red.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
White, kind things are cold.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is green and rough then it is cold.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Red, kind things are cold.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is cold and not white then it is green.
((("something" "is" "cold" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple2)]
("Anne" "is" "rough" "+")
triple2
Dave is rough.
False
1
inv-proof
[(triple14)]
("Dave" "is" "rough" "+")
triple14
Anne is kind.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple16) -> rule7))]
("Dave" "is" "green" "-")
((triple16) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is cold.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule4))]
("Anne" "is" "cold" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple16) -> rule7)) -> rule6))]
("Dave" "is" "kind" "-")
((((triple16) -> (rule7 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is green.
True
6
proof
[(((((triple1 ((triple2) -> rule5)) -> rule4) triple4) -> rule8))]
("Anne" "is" "green" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not green.
False
6
inv-proof
[(((((triple1 ((triple2) -> rule5)) -> rule4) triple4) -> rule8))]
("Anne" "is" "green" "-")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
@0: Anne is not round.[(triple3)] Anne is not white.[(triple4)] Anne is red.[(triple1)] Anne is rough.[(triple2)] Charlie is cold.[(triple5 OR ((triple11 triple7) -> rule2) OR ((triple6 triple9) -> rule3) OR ((triple11 ((triple6) -> rule6)) -> rule2) OR ((triple11 ((triple9) -> rule5)) -> rule2) OR ((((triple11) -> rule7) triple9) -> rule3) OR ((triple11 ((((triple11) -> rule7)) -> rule6)) -> rule2))] Charlie is green.[(triple6 OR ((triple11) -> rule7))] Charlie is kind.[(triple7 OR ((triple6) -> rule6) OR ((triple9) -> rule5) OR ((((triple11) -> rule7)) -> rule6))] Charlie is not red.[(triple8)] Charlie is not round.[(triple10)] Charlie is rough.[(triple9)] Charlie is white.[(triple11)] Dave is cold.[(triple12 OR ((triple13 ((((triple16) -> rule7)) -> rule6)) -> rule4) OR ((triple16 ((((triple16) -> rule7)) -> rule6)) -> rule2))] Dave is not rough.[(triple14)] Dave is not round.[(triple15)] Dave is red.[(triple13)] Dave is white.[(triple16)] @1: Anne is kind.[(((triple2) -> rule5))] Dave is green.[(((triple16) -> rule7))] @2: Anne is cold.[(((triple1 ((triple2) -> rule5)) -> rule4))] Dave is kind.[(((((triple16) -> rule7)) -> rule6))] @3: Anne is green.[(((((triple1 ((triple2) -> rule5)) -> rule4) triple4) -> rule8))]
Anne is not round.
("Anne" "is" "round" "-")
triple3
Anne is not white.
("Anne" "is" "white" "-")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((triple11 triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple6 triple9) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple11 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple11 ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple11) -> (rule7 % int2)) triple9) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple11 ((((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple11) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
((triple6) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple9) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
triple8
Charlie is not round.
("Charlie" "is" "round" "-")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple11
Dave is cold.
("Dave" "is" "cold" "+")
triple12
((triple13 ((((triple16) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((triple16 ((((triple16) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not rough.
("Dave" "is" "rough" "-")
triple14
Dave is not round.
("Dave" "is" "round" "-")
triple15
Dave is red.
("Dave" "is" "red" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple16
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple16) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple16) -> (rule7 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3