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