Bob is quiet. Charlie is furry. Dave is white. If someone is white then they are round. Quiet people are white. If Bob is rough and Bob is not round then Bob is not green. All quiet, white people are green. If someone is rough and not white then they are green. White, rough people are green. If someone is green and not round then they are young. If someone is green then they are young.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Bob is rough and Bob is not round then Bob is not green.
((("Bob" "is" "rough" "+") ("Bob" "is" "round" "~")) -> ("Bob" "is" "green" "-"))
All quiet, white people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and not white then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "+"))
White, rough people are green.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is green and not round then they are young.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Bob is white.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "white" "+")
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "round" "-")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Bob is green.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule8))]
("Bob" "is" "young" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule8))]
("Bob" "is" "young" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Dave" "is" "young" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is quiet.[(triple1)] Charlie is furry.[(triple2)] Dave is white.[(triple3)] @1: Bob is white.[(((triple1) -> rule2))] Dave is round.[(((triple3) -> rule1))] @2: Bob is green.[(((triple1 ((triple1) -> rule2)) -> rule4))] Bob is round.[(((((triple1) -> rule2)) -> rule1))] @3: Bob is young.[(((((triple1 ((triple1) -> rule2)) -> rule4)) -> rule8))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3