Dave is quiet. Gary is white. All nice people are quiet. White people are big. If someone is quiet then they are blue. All big people are nice. If someone is big then they are nice. If someone is round then they are quiet.
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Gary is white.
True
1
proof
[(triple2)]
("Gary" "is" "white" "+")
triple2
Gary is not white.
False
1
inv-proof
[(triple2)]
("Gary" "is" "white" "-")
triple2
Dave is blue.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "big" "-")
((triple2) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule2)) -> rule5))]
("Gary" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule2)) -> rule5))]
("Gary" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule5)) -> rule1))]
("Gary" "is" "quiet" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule5)) -> rule1))]
("Gary" "is" "quiet" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Dave" "is" "nice" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is quiet.[(triple1)] Gary is white.[(triple2)] @1: Dave is blue.[(((triple1) -> rule3))] Gary is big.[(((triple2) -> rule2))] @2: Gary is nice.[(((((triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule2)) -> rule5))] @3: Gary is quiet.[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule5)) -> rule1))] @4: Gary is blue.[(((((((((triple2) -> rule2)) -> rule4)) -> rule1)) -> rule3) OR ((((((((triple2) -> rule2)) -> rule5)) -> rule1)) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple2) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4