Bob is quiet. Bob is not red. Bob is rough. Bob is young. Charlie is round. Fiona is not green. Fiona is red. Fiona is rough. Fiona is not young. Gary is red. Gary is rough. Gary is young. All white, red people are green. All white people are green. If someone is green and young then they are red. If Gary is red then Gary is young. All round people are white. If Charlie is green and Charlie is rough then Charlie is young. If someone is quiet then they are young. All green, round people are young. Red, round people are not quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
All white, red people are green.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is green and young then they are red.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Gary is red then Gary is young.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "young" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Charlie is green and Charlie is rough then Charlie is young.
((("Charlie" "is" "green" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All green, round people are young.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Red, round people are not quiet.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
Bob is young.
True
1
proof
[(triple4 OR ((triple1) -> rule7))]
("Bob" "is" "young" "+")
triple4
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is not red.
False
1
inv-proof
[(triple10)]
("Gary" "is" "red" "-")
triple10
Charlie is white.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "white" "+")
((triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple5) -> rule5))]
("Charlie" "is" "white" "-")
((triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
True
3
proof
[(((((triple5) -> rule5)) -> rule2))]
("Charlie" "is" "green" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule2))]
("Charlie" "is" "green" "-")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
True
5
proof
[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule8))]
("Charlie" "is" "young" "+")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule8))]
("Charlie" "is" "young" "-")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is red.
True
9
proof
[(((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3))]
("Charlie" "is" "red" "+")
((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) triple5) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not red.
False
9
inv-proof
[(((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3))]
("Charlie" "is" "red" "-")
((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) triple5) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not quiet.
True
11
proof
[(((((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3) triple5) -> rule9))]
("Charlie" "is" "quiet" "-")
((((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) triple5) -> (rule8 % int3))) -> (rule3 % int2)) triple5) -> (rule9 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Charlie is quiet.
False
11
inv-proof
[(((((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3) triple5) -> rule9))]
("Charlie" "is" "quiet" "+")
((((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) triple5) -> (rule8 % int3))) -> (rule3 % int2)) triple5) -> (rule9 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is not red.[(triple2)] Bob is quiet.[(triple1)] Bob is rough.[(triple3)] Bob is young.[(triple4 OR ((triple1) -> rule7))] Charlie is round.[(triple5)] Fiona is not green.[(triple6)] Fiona is not young.[(triple9)] Fiona is red.[(triple7)] Fiona is rough.[(triple8)] Gary is red.[(triple10)] Gary is rough.[(triple11)] Gary is young.[(triple12 OR ((triple10) -> rule4))] @1: Charlie is white.[(((triple5) -> rule5))] @2: Charlie is green.[(((((triple5) -> rule5)) -> rule2))] @3: Charlie is young.[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule8))] @4: Charlie is red.[(((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3))] @5: Charlie is not quiet.[(((((((((triple5) -> rule5)) -> rule2) ((((((triple5) -> rule5)) -> rule2) triple5) -> rule8)) -> rule3) triple5) -> rule9))]
Bob is not red.
("Bob" "is" "red" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Fiona is not green.
("Fiona" "is" "green" "-")
triple6
Fiona is not young.
("Fiona" "is" "young" "-")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple10) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) ((((((triple5) -> (rule5 % int4))) -> (rule2 % int3)) triple5) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) ((((((triple5) -> (rule5 % int5))) -> (rule2 % int4)) triple5) -> (rule8 % int3))) -> (rule3 % int2)) triple5) -> (rule9 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5