Anne is nice. Bob is young. Erin is not white. Gary is young. All young people are rough. All rough people are big. If someone is rough and not red then they are big. If Bob is not red then Bob is young. If Gary is kind then Gary is white. All big people are not nice.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is not white.
("Erin" "is" "white" "-")
Gary is young.
("Gary" "is" "young" "+")
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and not red then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
If Bob is not red then Bob is young.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "young" "+"))
If Gary is kind then Gary is white.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "white" "+"))
All big people are not nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
Erin is not white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Gary is rough.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "rough" "-")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "big" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not nice.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
("Gary" "is" "nice" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
("Gary" "is" "nice" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is nice.[(triple1)] Bob is young.[(triple2)] Erin is not white.[(triple3)] Gary is young.[(triple4)] @1: Bob is rough.[(((triple2) -> rule1))] Gary is rough.[(((triple4) -> rule1))] @2: Bob is big.[(((((triple2) -> rule1)) -> rule2))] Gary is big.[(((((triple4) -> rule1)) -> rule2))] @3: Bob is not nice.[(((((((triple2) -> rule1)) -> rule2)) -> rule6))] Gary is not nice.[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Erin is not white.
("Erin" "is" "white" "-")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Bob is not nice.
("Bob" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Gary is not nice.
("Gary" "is" "nice" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3