Dave is green. Fiona is cold. If something is big and nice then it is furry. All rough things are nice. If something is rough and not big then it is nice. If Dave is white then Dave is green. If Fiona is cold then Fiona is rough. If something is white then it is rough. If something is furry then it is white. If Fiona is not white then Fiona is green.
Dave is green.
("Dave" "is" "green" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If something is big and nice then it is furry.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is rough and not big then it is nice.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
If Dave is white then Dave is green.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "+"))
If Fiona is cold then Fiona is rough.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "rough" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Fiona is not white then Fiona is green.
((("Fiona" "is" "white" "~")) -> ("Fiona" "is" "green" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Fiona is not cold.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "cold" "-")
triple2
Fiona is rough.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Fiona" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Fiona" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "white" "+")
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Dave is green.[(triple1)] Fiona is cold.[(triple2)] @1: Fiona is rough.[(((triple2) -> rule5))] @2: Fiona is nice.[(((((triple2) -> rule5)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2