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