Bob is red. Rough people are round. If someone is round then they are kind. If Bob is young then Bob is red. If Bob is green then Bob is round. If someone is green then they are rough. If Bob is red then Bob is green.
Bob is red.
("Bob" "is" "red" "+")
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Bob is young then Bob is red.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "red" "+"))
If Bob is green then Bob is round.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "round" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Bob is red then Bob is green.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "green" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is green.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "green" "+")
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "green" "-")
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule5)) -> rule1))]
("Bob" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not rough.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
True
4
proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule2) OR ((((((((triple1) -> rule6)) -> rule5)) -> rule1)) -> rule2))]
("Bob" "is" "kind" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not kind.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule2) OR ((((((((triple1) -> rule6)) -> rule5)) -> rule1)) -> rule2))]
("Bob" "is" "kind" "-")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is red.[(triple1)] @1: Bob is green.[(((triple1) -> rule6))] @2: Bob is rough.[(((((triple1) -> rule6)) -> rule5))] Bob is round.[(((((triple1) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule5)) -> rule1))] @3: Bob is kind.[(((((((triple1) -> rule6)) -> rule4)) -> rule2) OR ((((((((triple1) -> rule6)) -> rule5)) -> rule1)) -> rule2))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4