Dave is round. Fiona is not cold. Fiona is green. Fiona is quiet. Fiona is round. Fiona is white. Gary is not white. All round, quiet people are green. Round, green people are not kind. Round people are quiet. If Gary is cold then Gary is quiet. All kind, white people are not furry. All kind people are not white.
Dave is round.
("Dave" "is" "round" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is not white.
("Gary" "is" "white" "-")
All round, quiet people are green.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Round, green people are not kind.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "-"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is cold then Gary is quiet.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "quiet" "+"))
All kind, white people are not furry.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "-"))
All kind people are not white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "-"))
Fiona is white.
True
1
proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Dave is not round.
False
1
inv-proof
[(triple1)]
("Dave" "is" "round" "-")
triple1
Fiona is not kind.
True
3
proof
[(((triple5 triple3) -> rule2) OR ((triple5 ((triple5 triple4) -> rule1)) -> rule2) OR ((triple5 ((triple5 ((triple5) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "kind" "-")
((triple5 triple3) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
((triple5 ((triple5 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple5 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Dave" "is" "green" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Dave" "is" "green" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not kind.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is kind.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
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" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is round.[(triple1)] Fiona is green.[(triple3 OR ((triple5 triple4) -> rule1) OR ((triple5 ((triple5) -> rule3)) -> rule1))] Fiona is not cold.[(triple2)] Fiona is quiet.[(triple4 OR ((triple5) -> rule3))] Fiona is round.[(triple5)] Fiona is white.[(triple6)] Gary is not white.[(triple7)] @1: Dave is quiet.[(((triple1) -> rule3))] Fiona is not kind.[(((triple5 triple3) -> rule2) OR ((triple5 ((triple5 triple4) -> rule1)) -> rule2) OR ((triple5 ((triple5 ((triple5) -> rule3)) -> rule1)) -> rule2))] @2: Dave is green.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: Dave is not kind.[(((triple1 ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((triple5 triple4) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
((triple5) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Gary is not white.
("Gary" "is" "white" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is not kind.
("Fiona" "is" "kind" "-")
((triple5 triple3) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
((triple5 ((triple5 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple5 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
((triple1 ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3