Bob is furry. Dave is round. Erin is nice. Round, white people are furry. If Bob is round then Bob is rough. If someone is nice and white then they are round. If someone is round then they are green. All rough people are nice. All green people are rough. If someone is nice and smart then they are round. If someone is nice and rough then they are smart.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Round, white people are furry.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Bob is round then Bob is rough.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "rough" "+"))
If someone is nice and white then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and smart then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and rough then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "-")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "nice" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "nice" "-")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@5: Erin is round.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule6 <- rule4 <- rule3 <- FAIL)]]
("Erin" "is" "round" "-")
Bob is rough.
Unknown
rconc
[@6: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule5 <- rule6 <- rule4 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Erin is rough.
Unknown
rconc
[@4: Erin is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule7 <- rule8 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is furry.[(triple1)] Dave is round.[(triple2)] Erin is nice.[(triple3)] @1: Dave is green.[(((triple2) -> rule4))] @2: Dave is rough.[(((((triple2) -> rule4)) -> rule6))] @3: Dave is nice.[(((((((triple2) -> rule4)) -> rule6)) -> rule5))] @4: Dave is smart.[(((((((((triple2) -> rule4)) -> rule6)) -> rule5) ((((triple2) -> rule4)) -> rule6)) -> rule8))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4