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