Bob is young. All young people are green. If someone is smart and not round then they are red. Green people are red. If Bob is green and Bob is red then Bob is furry. If someone is round then they are not furry. If someone is red then they are furry. Round people are furry. If someone is smart then they are not young.
Bob is young.
("Bob" "is" "young" "+")
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not round then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Bob is green and Bob is red then Bob is furry.
((("Bob" "is" "green" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "furry" "+"))
If someone is round then they are not furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "-"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are not young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "-"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Bob is green.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "green" "-")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is young.[(triple1)] @1: Bob is green.[(((triple1) -> rule1))] @2: Bob is red.[(((((triple1) -> rule1)) -> rule3))] @3: Bob is furry.[(((((((triple1) -> rule1)) -> rule3)) -> rule6) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3