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