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