Bob is rough. Charlie is white. Dave is red. Erin is red. All green things are round. If something is kind then it is green. If something is rough then it is green. If something is rough and furry then it is white. If something is green and round then it is kind. Round things are green. Green, kind things are rough. If something is furry and red then it is rough.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is rough and furry then it is white.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is green and round then it is kind.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Green, kind things are rough.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is furry and red then it is rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Dave is red.
True
1
proof
[(triple3)]
("Dave" "is" "red" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple4)]
("Erin" "is" "red" "-")
triple4
Bob is green.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "-")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule5))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@4: Dave is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule7 <- rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@4: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Erin is not green.
Unknown
inv-rconc
[@5: Erin is green.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- rule3 <- rule7 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@5: Charlie is green.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is rough.[(triple1)] Charlie is white.[(triple2)] Dave is red.[(triple3)] Erin is red.[(triple4)] @1: Bob is green.[(((triple1) -> rule3))] @2: Bob is round.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is kind.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3