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