Anne is round. Charlie is white. Erin is round. Gary is white. Round things are nice. If something is big and nice then it is young. If something is young then it is rough. If Anne is nice then Anne is big. If something is blue and white then it is nice. If something is blue then it is nice.
Anne is round.
("Anne" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is big and nice then it is young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Anne is nice then Anne is big.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If something is blue and white then it is nice.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Charlie is white.
True
1
proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "-")
triple2
Erin is nice.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
True
6
proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not young.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is round.[(triple1)] Charlie is white.[(triple2)] Erin is round.[(triple3)] Gary is white.[(triple4)] @1: Anne is nice.[(((triple1) -> rule1))] Erin is nice.[(((triple3) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule4))] @3: Anne is young.[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule2))] @4: Anne is rough.[(((((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) ((triple1) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4