Gary is white. If something is white then it is big. Big, white things are round. All big things are round. If something is big and quiet then it is round. All quiet things are green. If Gary is green then Gary is smart. If something is white and round then it is not quiet. If Gary is blue and Gary is big then Gary is round.
Gary is white.
("Gary" "is" "white" "+")
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Big, white things are round.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is big and quiet then it is round.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Gary is green then Gary is smart.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "smart" "+"))
If something is white and round then it is not quiet.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "-"))
If Gary is blue and Gary is big then Gary is round.
((("Gary" "is" "blue" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "round" "+"))
Gary is white.
True
1
proof
[(triple1)]
("Gary" "is" "white" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple1)]
("Gary" "is" "white" "-")
triple1
Gary is big.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "big" "+")
((triple1) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Gary" "is" "big" "-")
((triple1) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1) triple1) -> rule2))]
("Gary" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1) triple1) -> rule2))]
("Gary" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not quiet.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule7) OR ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule7) OR ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "green" "+")
@0: Gary is white.[(triple1)] @1: Gary is big.[(((triple1) -> rule1))] @2: Gary is round.[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1) triple1) -> rule2))] @3: Gary is not quiet.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule7) OR ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule7))]
Gary is white.
("Gary" "is" "white" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
((triple1) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3