Anne is smart. Charlie is not green. Dave is red. Erin is quiet. If something is cold then it is green. If something is smart and not round then it is green. If Dave is green and Dave is not rough then Dave is smart. If something is red then it is cold. Quiet things are red. If Erin is not smart then Erin is red.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is smart and not round then it is green.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "+"))
If Dave is green and Dave is not rough then Dave is smart.
((("Dave" "is" "green" "+") ("Dave" "is" "rough" "~")) -> ("Dave" "is" "smart" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Erin is not smart then Erin is red.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "red" "+"))
Charlie is not green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Erin is red.
True
2
proof
[(((triple4) -> rule5))]
("Erin" "is" "red" "+")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Erin" "is" "red" "-")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Dave is green.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("Dave" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("Dave" "is" "green" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is green.
True
4
proof
[(((((((triple4) -> rule5)) -> rule4)) -> rule1))]
("Erin" "is" "green" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not green.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule4)) -> rule1))]
("Erin" "is" "green" "-")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is smart.[(triple1)] Charlie is not green.[(triple2)] Dave is red.[(triple3)] Erin is quiet.[(triple4)] @1: Dave is cold.[(((triple3) -> rule4))] Erin is red.[(((triple4) -> rule5))] @2: Dave is green.[(((((triple3) -> rule4)) -> rule1))] Erin is cold.[(((((triple4) -> rule5)) -> rule4))] @3: Erin is green.[(((((((triple4) -> rule5)) -> rule4)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3