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