Anne is round. Bob is smart. If someone is quiet then they are green. All smart people are red. If Anne is blue then Anne is young. Green, round people are quiet. Red people are quiet. Smart people are red.
Anne is round.
("Anne" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If Anne is blue then Anne is young.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "young" "+"))
Green, round people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Bob is red.
True
2
proof
[(((triple2) -> rule2) OR ((triple2) -> rule6))]
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple2) -> rule6))]
("Bob" "is" "red" "-")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule5) OR ((((triple2) -> rule6)) -> rule5))]
("Bob" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5) OR ((((triple2) -> rule6)) -> rule5))]
("Bob" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule1) OR ((((((triple2) -> rule6)) -> rule5)) -> rule1))]
("Bob" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule1) OR ((((((triple2) -> rule6)) -> rule5)) -> rule1))]
("Bob" "is" "green" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@4: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule5 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is green.
Unknown
rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is round.[(triple1)] Bob is smart.[(triple2)] @1: Bob is red.[(((triple2) -> rule2) OR ((triple2) -> rule6))] @2: Bob is quiet.[(((((triple2) -> rule2)) -> rule5) OR ((((triple2) -> rule6)) -> rule5))] @3: Bob is green.[(((((((triple2) -> rule2)) -> rule5)) -> rule1) OR ((((((triple2) -> rule6)) -> rule5)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3