Anne is cold. Anne is furry. Anne is green. Anne is round. Fiona is blue. Fiona is cold. Fiona is furry. Fiona is green. Fiona is red. Fiona is round. If Fiona is cold and Fiona is smart then Fiona is blue. If something is red then it is smart. If something is round and green then it is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If Fiona is cold and Fiona is smart then Fiona is blue.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "blue" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is round and green then it is cold.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Fiona is blue.
True
1
proof
[(triple5 OR ((triple6 ((triple9) -> rule2)) -> rule1) OR ((((triple10 triple8) -> rule3) ((triple9) -> rule2)) -> rule1))]
("Fiona" "is" "blue" "+")
triple5
((triple6 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple8) -> (rule3 % int3)) ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Anne is not green.
False
1
inv-proof
[(triple3)]
("Anne" "is" "green" "-")
triple3
Fiona is smart.
True
2
proof
[(((triple9) -> rule2))]
("Fiona" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple9) -> rule2))]
("Fiona" "is" "smart" "-")
((triple9) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is cold.[(triple1 OR ((triple4 triple3) -> rule3))] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is round.[(triple4)] Fiona is blue.[(triple5 OR ((triple6 ((triple9) -> rule2)) -> rule1) OR ((((triple10 triple8) -> rule3) ((triple9) -> rule2)) -> rule1))] Fiona is cold.[(triple6 OR ((triple10 triple8) -> rule3))] Fiona is furry.[(triple7)] Fiona is green.[(triple8)] Fiona is red.[(triple9)] Fiona is round.[(triple10)] @1: Fiona is smart.[(((triple9) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple4 triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple6 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple8) -> (rule3 % int3)) ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple10 triple8) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1