Anne is not green. Bob is green. Charlie is rough. Dave is green. If Charlie is blue then Charlie is green. Green, blue people are round. Rough people are blue.
Anne is not green.
("Anne" "is" "green" "-")
Bob is green.
("Bob" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is green.
("Dave" "is" "green" "+")
If Charlie is blue then Charlie is green.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "green" "+"))
Green, blue people are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Dave is green.
True
1
proof
[(triple4)]
("Dave" "is" "green" "+")
triple4
Dave is not green.
False
1
inv-proof
[(triple4)]
("Dave" "is" "green" "-")
triple4
Charlie is blue.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Charlie" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Charlie" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
True
6
proof
[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
("Charlie" "is" "round" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not round.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
("Charlie" "is" "round" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "+")
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is not green.[(triple1)] Bob is green.[(triple2)] Charlie is rough.[(triple3)] Dave is green.[(triple4)] @1: Charlie is blue.[(((triple3) -> rule3))] @2: Charlie is green.[(((((triple3) -> rule3)) -> rule1))] @3: Charlie is round.[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3