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