Anne is not young. Charlie is not rough. Dave is smart. Gary is rough. All green, smart things are red. Smart things are green. If something is nice and not green then it is not big.
Anne is not young.
("Anne" "is" "young" "-")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is nice and not green then it is not big.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "-"))
Gary is rough.
True
1
proof
[(triple4)]
("Gary" "is" "rough" "+")
triple4
Gary is not rough.
False
1
inv-proof
[(triple4)]
("Gary" "is" "rough" "-")
triple4
Dave is green.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "-")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not red.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Dave" "is" "red" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is not young.[(triple1)] Charlie is not rough.[(triple2)] Dave is smart.[(triple3)] Gary is rough.[(triple4)] @1: Dave is green.[(((triple3) -> rule2))] @2: Dave is red.[(((((triple3) -> rule2) triple3) -> rule1))]
Anne is not young.
("Anne" "is" "young" "-")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2