Anne is not white. Charlie is nice. Dave is rough. Erin is kind. If something is big and kind then it is white. Red things are white. Big things are kind. If something is young and not nice then it is kind. Kind things are red. If something is kind then it is rough. If something is young and not white then it is not rough. All big things are rough.
Anne is not white.
("Anne" "is" "white" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If something is big and kind then it is white.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is young and not nice then it is kind.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is young and not white then it is not rough.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "-"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple4)]
("Erin" "is" "kind" "-")
triple4
Erin is rough.
True
2
proof
[(((triple4) -> rule6))]
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Erin" "is" "red" "-")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("Erin" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("Erin" "is" "white" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is not white.[(triple1)] Charlie is nice.[(triple2)] Dave is rough.[(triple3)] Erin is kind.[(triple4)] @1: Erin is red.[(((triple4) -> rule5))] Erin is rough.[(((triple4) -> rule6))] @2: Erin is white.[(((((triple4) -> rule5)) -> rule2))]
Anne is not white.
("Anne" "is" "white" "-")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2