Anne is green. Anne is quiet. Anne is smart. Erin is cold. Erin is red. Fiona is green. Fiona is smart. Fiona is white. Harry is quiet. Harry is red. All green, red things are white. If Fiona is green then Fiona is red. All smart, cold things are quiet. All red, white things are cold. All green, cold things are red. All white, smart things are nice.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
All green, red things are white.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Fiona is green then Fiona is red.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "red" "+"))
All smart, cold things are quiet.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All red, white things are cold.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All green, cold things are red.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All white, smart things are nice.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Fiona is white.
True
1
proof
[(triple8 OR ((triple6 ((triple6) -> rule2)) -> rule1))]
("Fiona" "is" "white" "+")
triple8
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Anne is not smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Fiona is red.
True
2
proof
[(((triple6) -> rule2))]
("Fiona" "is" "red" "+")
((triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not nice.
False
3
inv-proof
[(((triple8 triple7) -> rule6) OR ((((triple6 ((triple6) -> rule2)) -> rule1) triple7) -> rule6))]
("Fiona" "is" "nice" "-")
((triple8 triple7) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is cold.
True
4
proof
[(((((triple6) -> rule2) triple8) -> rule4) OR ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4))]
("Fiona" "is" "cold" "+")
((((triple6) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not cold.
False
4
inv-proof
[(((((triple6) -> rule2) triple8) -> rule4) OR ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4))]
("Fiona" "is" "cold" "-")
((((triple6) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is quiet.
True
6
proof
[(((triple7 ((((triple6) -> rule2) triple8) -> rule4)) -> rule3) OR ((triple7 ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule3))]
("Fiona" "is" "quiet" "+")
((triple7 ((((triple6) -> (rule2 % int3)) triple8) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((triple7 ((((triple6) -> (rule2 % int4)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is not quiet.
False
6
inv-proof
[(((triple7 ((((triple6) -> rule2) triple8) -> rule4)) -> rule3) OR ((triple7 ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule3))]
("Fiona" "is" "quiet" "-")
((triple7 ((((triple6) -> (rule2 % int3)) triple8) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((triple7 ((((triple6) -> (rule2 % int4)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "+")
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is white.
Unknown
rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- FAIL)]]
("Anne" "is" "white" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3)] Erin is cold.[(triple4)] Erin is red.[(triple5)] Fiona is green.[(triple6)] Fiona is smart.[(triple7)] Fiona is white.[(triple8 OR ((triple6 ((triple6) -> rule2)) -> rule1))] Harry is quiet.[(triple9)] Harry is red.[(triple10)] @1: Fiona is nice.[(((triple8 triple7) -> rule6) OR ((((triple6 ((triple6) -> rule2)) -> rule1) triple7) -> rule6))] Fiona is red.[(((triple6) -> rule2))] @2: Fiona is cold.[(((((triple6) -> rule2) triple8) -> rule4) OR ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4))] @3: Fiona is quiet.[(((triple7 ((((triple6) -> rule2) triple8) -> rule4)) -> rule3) OR ((triple7 ((((triple6) -> rule2) ((triple6 ((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple8 triple7) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple6) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple6 ((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7 ((((triple6) -> (rule2 % int3)) triple8) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((triple7 ((((triple6) -> (rule2 % int4)) ((triple6 ((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4