Dave is cold. Fiona is nice. Fiona is round. If Dave is green then Dave is blue. If something is blue and cold then it is nice. If something is cold then it is round. If Fiona is cold and Fiona is blue then Fiona is furry. If something is blue then it is furry. If something is blue and green then it is cold. If Fiona is nice then Fiona is white. Round things are nice.
Dave is cold.
("Dave" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If Dave is green then Dave is blue.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "blue" "+"))
If something is blue and cold then it is nice.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Fiona is cold and Fiona is blue then Fiona is furry.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "furry" "+"))
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is blue and green then it is cold.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Fiona is nice then Fiona is white.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "white" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple2 OR ((triple3) -> rule8))]
("Fiona" "is" "nice" "+")
triple2
((triple3) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is round.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "round" "+")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "round" "-")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is furry.
Unknown
rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Dave is cold.[(triple1)] Fiona is nice.[(triple2 OR ((triple3) -> rule8))] Fiona is round.[(triple3)] @1: Dave is round.[(((triple1) -> rule3))] Fiona is white.[(((triple2) -> rule7) OR ((((triple3) -> rule8)) -> rule7))] @2: Dave is nice.[(((((triple1) -> rule3)) -> rule8))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
((triple3) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2