Anne is blue. Anne is green. Anne is quiet. Anne is round. Bob is blue. Bob is cold. Bob is kind. Bob is quiet. Bob is round. Fiona is blue. Fiona is cold. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is red. Fiona is round. Cold, kind things are round. If something is quiet then it is kind. All cold, kind things are blue. Quiet, cold things are red. If something is round and green then it is blue. If Anne is kind and Anne is blue then Anne is cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Cold, kind things are round.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All cold, kind things are blue.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Quiet, cold things are red.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is round and green then it is blue.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Anne is kind and Anne is blue then Anne is cold.
((("Anne" "is" "kind" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple4 triple2) -> rule5))]
("Anne" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is not round.
False
1
inv-proof
[(triple9 OR ((triple6 triple7) -> rule1) OR ((triple6 ((triple8) -> rule2)) -> rule1))]
("Bob" "is" "round" "-")
triple9
((triple6 triple7) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Anne is kind.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
True
4
proof
[(((((triple3) -> rule2) triple1) -> rule6) OR ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6))]
("Anne" "is" "cold" "+")
((((triple3) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple4 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((((triple3) -> rule2) triple1) -> rule6) OR ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6))]
("Anne" "is" "cold" "-")
((((triple3) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple4 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
True
6
proof
[(((triple3 ((((triple3) -> rule2) triple1) -> rule6)) -> rule4) OR ((triple3 ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "red" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple3 ((((triple3) -> (rule2 % int4)) ((triple4 triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is not red.
False
6
inv-proof
[(((triple3 ((((triple3) -> rule2) triple1) -> rule6)) -> rule4) OR ((triple3 ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "red" "-")
((triple3 ((((triple3) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple3 ((((triple3) -> (rule2 % int4)) ((triple4 triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
@0: Anne is blue.[(triple1 OR ((triple4 triple2) -> rule5))] Anne is green.[(triple2)] Anne is quiet.[(triple3)] Anne is round.[(triple4 OR ((((((triple3) -> rule2) triple1) -> rule6) ((triple3) -> rule2)) -> rule1))] Bob is blue.[(triple5 OR ((triple6 triple7) -> rule3) OR ((triple6 ((triple8) -> rule2)) -> rule3))] Bob is cold.[(triple6)] Bob is kind.[(triple7 OR ((triple8) -> rule2))] Bob is quiet.[(triple8)] Bob is round.[(triple9 OR ((triple6 triple7) -> rule1) OR ((triple6 ((triple8) -> rule2)) -> rule1))] Fiona is blue.[(triple10 OR ((triple11 triple13) -> rule3) OR ((triple16 triple12) -> rule5) OR ((triple11 ((triple14) -> rule2)) -> rule3) OR ((((triple11 triple13) -> rule1) triple12) -> rule5) OR ((((triple11 ((triple14) -> rule2)) -> rule1) triple12) -> rule5))] Fiona is cold.[(triple11)] Fiona is green.[(triple12)] Fiona is kind.[(triple13 OR ((triple14) -> rule2))] Fiona is quiet.[(triple14)] Fiona is red.[(triple15 OR ((triple14 triple11) -> rule4))] Fiona is round.[(triple16 OR ((triple11 triple13) -> rule1) OR ((triple11 ((triple14) -> rule2)) -> rule1))] @1: Anne is kind.[(((triple3) -> rule2))] Bob is red.[(((triple8 triple6) -> rule4))] @2: Anne is cold.[(((((triple3) -> rule2) triple1) -> rule6) OR ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6))] @3: Anne is red.[(((triple3 ((((triple3) -> rule2) triple1) -> rule6)) -> rule4) OR ((triple3 ((((triple3) -> rule2) ((triple4 triple2) -> rule5)) -> rule6)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((((((triple3) -> (rule2 % int3)) triple1) -> (rule6 % int2)) ((triple3) -> (rule2 % int3))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple5
((triple6 triple7) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
((triple8) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple9
((triple6 triple7) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple10
((triple11 triple13) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple16 triple12) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple11 ((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple11 triple13) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple11 ((triple14) -> (rule2 % int3))) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
triple12
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
((triple14) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
Fiona is red.
("Fiona" "is" "red" "+")
triple15
((triple14 triple11) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple16
((triple11 triple13) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple11 ((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple8 triple6) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple3) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple4 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple3 ((((triple3) -> (rule2 % int4)) ((triple4 triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4