Dave is blue. Erin is green. If something is blue and furry then it is green. If something is nice then it is green. If Dave is not red then Dave is not green. Blue things are quiet. If something is red and not blue then it is furry. If Dave is nice then Dave is not quiet. If Dave is quiet then Dave is furry. If something is green then it is white.
Dave is blue.
("Dave" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
If something is blue and furry then it is green.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Dave is not red then Dave is not green.
((("Dave" "is" "red" "~")) -> ("Dave" "is" "green" "-"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is red and not blue then it is furry.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "furry" "+"))
If Dave is nice then Dave is not quiet.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "-"))
If Dave is quiet then Dave is furry.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "furry" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Erin is white.
True
2
proof
[(((triple2) -> rule8))]
("Erin" "is" "white" "+")
((triple2) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Dave is blue.[(triple1)] Erin is green.[(triple2)] @1: Dave is quiet.[(((triple1) -> rule4))] Erin is white.[(((triple2) -> rule8))] @2: Dave is furry.[(((((triple1) -> rule4)) -> rule7))] @3: Dave is green.[(((triple1 ((((triple1) -> rule4)) -> rule7)) -> rule1))] @4: Dave is white.[(((((triple1 ((((triple1) -> rule4)) -> rule7)) -> rule1)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4