Dave is nice. Fiona is round. Gary is quiet. If Gary is white and Gary is quiet then Gary is round. If someone is kind and round then they are not quiet. White, nice people are not quiet. If someone is quiet then they are kind. Nice people are kind. All quiet people are not green. All kind people are not red. If someone is kind and nice then they are round.
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Gary is white and Gary is quiet then Gary is round.
((("Gary" "is" "white" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "round" "+"))
If someone is kind and round then they are not quiet.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
White, nice people are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "-"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are not green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
All kind people are not red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
If someone is kind and nice then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Fiona is round.
True
1
proof
[(triple2)]
("Fiona" "is" "round" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "round" "-")
triple2
Dave is kind.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Gary is green.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "green" "+")
((triple3) -> (rule6 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Dave is not red.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("Dave" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is red.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule7))]
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is not quiet.
True
7
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule8)) -> rule2))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is quiet.
False
7
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule8)) -> rule2))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Dave is nice.[(triple1)] Fiona is round.[(triple2)] Gary is quiet.[(triple3)] @1: Dave is kind.[(((triple1) -> rule5))] Gary is kind.[(((triple3) -> rule4))] Gary is not green.[(((triple3) -> rule6))] @2: Dave is not red.[(((((triple1) -> rule5)) -> rule7))] Dave is round.[(((((triple1) -> rule5) triple1) -> rule8))] Gary is not red.[(((((triple3) -> rule4)) -> rule7))] @3: Dave is not quiet.[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule8)) -> rule2))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
((triple3) -> (rule6 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is not red.
("Gary" "is" "red" "-")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3