Anne is big. Anne is cold. Dave is furry. Dave is nice. Fiona is cold. Fiona is green. Fiona is nice. If Fiona is furry then Fiona is nice. Nice people are white. All green, nice people are not furry. Furry, nice people are cold. If someone is nice and green then they are cold. If Fiona is green and Fiona is not white then Fiona is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Fiona is furry then Fiona is nice.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "nice" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All green, nice people are not furry.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
Furry, nice people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and green then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is green and Fiona is not white then Fiona is young.
((("Fiona" "is" "green" "+") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "young" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Fiona is not cold.
False
1
inv-proof
[(triple5 OR ((triple7 triple6) -> rule5))]
("Fiona" "is" "cold" "-")
triple5
((triple7 triple6) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "white" "+")
((triple7) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Dave is not cold.
False
3
inv-proof
[(((triple3 triple4) -> rule4))]
("Dave" "is" "cold" "-")
((triple3 triple4) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4)] Fiona is cold.[(triple5 OR ((triple7 triple6) -> rule5))] Fiona is green.[(triple6)] Fiona is nice.[(triple7)] @1: Dave is cold.[(((triple3 triple4) -> rule4))] Dave is white.[(((triple4) -> rule2))] Fiona is not furry.[(((triple6 triple7) -> rule3))] Fiona is white.[(((triple7) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
((triple7 triple6) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
((triple3 triple4) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is not furry.
("Fiona" "is" "furry" "-")
((triple6 triple7) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple7) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1