Anne is quiet. Charlie is not rough. Erin is smart. Fiona is rough. All smart, rough people are not green. If someone is red and not kind then they are rough. If someone is red and smart then they are rough. If someone is rough then they are not blue. All quiet people are smart. All blue people are red. If someone is smart then they are red. If someone is kind then they are red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All smart, rough people are not green.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is red and not kind then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "+"))
If someone is red and smart then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
Anne is smart.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Charlie is not rough.[(triple2)] Erin is smart.[(triple3)] Fiona is rough.[(triple4)] @1: Anne is smart.[(((triple1) -> rule5))] Erin is red.[(((triple3) -> rule7))] Fiona is not blue.[(((triple4) -> rule4))] @2: Anne is red.[(((((triple1) -> rule5)) -> rule7))] Erin is rough.[(((((triple3) -> rule7) triple3) -> rule3))] @3: Anne is rough.[(((((((triple1) -> rule5)) -> rule7) ((triple1) -> rule5)) -> rule3))] Erin is not blue.[(((((((triple3) -> rule7) triple3) -> rule3)) -> rule4))] Erin is not green.[(((triple3 ((((triple3) -> rule7) triple3) -> rule3)) -> rule1))] @4: Anne is not blue.[(((((((((triple1) -> rule5)) -> rule7) ((triple1) -> rule5)) -> rule3)) -> rule4))] Anne is not green.[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7) ((triple1) -> rule5)) -> rule3)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
((triple4) -> (rule4 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple3) -> (rule7 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not green.
("Erin" "is" "green" "-")
((triple3 ((((triple3) -> (rule7 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Anne is not blue.
("Anne" "is" "blue" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not green.
("Anne" "is" "green" "-")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4