Anne is not green. Dave is red. Erin is smart. If Erin is rough then Erin is young. If someone is rough then they are quiet. Green people are quiet. If someone is blue then they are quiet. If someone is quiet and rough then they are not green. If someone is smart then they are not green. All young people are red. If someone is red then they are rough.
Anne is not green.
("Anne" "is" "green" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is rough then Erin is young.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "young" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and rough then they are not green.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is smart then they are not green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "-"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
Dave is rough.
True
2
proof
[(((triple2) -> rule8))]
("Dave" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule8))]
("Dave" "is" "rough" "-")
((triple2) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple2) -> rule8)) -> rule2))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule2))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not green.
True
6
proof
[(((((((triple2) -> rule8)) -> rule2) ((triple2) -> rule8)) -> rule5))]
("Dave" "is" "green" "-")
((((((triple2) -> (rule8 % int3))) -> (rule2 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is green.
False
6
inv-proof
[(((((((triple2) -> rule8)) -> rule2) ((triple2) -> rule8)) -> rule5))]
("Dave" "is" "green" "+")
((((((triple2) -> (rule8 % int3))) -> (rule2 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is red.
Unknown
rconc
[@3: Erin is red.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule8 <- FAIL)]]
("Erin" "is" "red" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is not green.[(triple1)] Dave is red.[(triple2)] Erin is smart.[(triple3)] @1: Dave is rough.[(((triple2) -> rule8))] Erin is not green.[(((triple3) -> rule6))] @2: Dave is quiet.[(((((triple2) -> rule8)) -> rule2))] @3: Dave is not green.[(((((((triple2) -> rule8)) -> rule2) ((triple2) -> rule8)) -> rule5))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
((triple3) -> (rule6 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not green.
("Dave" "is" "green" "-")
((((((triple2) -> (rule8 % int3))) -> (rule2 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3