Bob is rough. Dave is young. Erin is not round. Erin is smart. Gary is rough. Gary is round. Gary is young. All rough, green things are white. Young things are white. White things are quiet. If something is quiet then it is rough. If something is young and not round then it is not green. If something is quiet and young then it is green.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough, green things are white.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is young and not round then it is not green.
((("something" "is" "young" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "-"))
If something is quiet and young then it is green.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Gary is rough.
True
1
proof
[(triple5 OR ((((((triple7) -> rule2)) -> rule3)) -> rule4))]
("Gary" "is" "rough" "+")
triple5
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not rough.
False
1
inv-proof
[(triple5 OR ((((((triple7) -> rule2)) -> rule3)) -> rule4))]
("Gary" "is" "rough" "-")
triple5
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is white.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "white" "+")
((triple7) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "white" "-")
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is green.
True
5
proof
[(((((((triple2) -> rule2)) -> rule3) triple2) -> rule6))]
("Dave" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not rough.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule4))]
("Dave" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is quiet.
Unknown
rconc
[@3: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is rough.[(triple1)] Dave is young.[(triple2)] Erin is not round.[(triple3)] Erin is smart.[(triple4)] Gary is rough.[(triple5 OR ((((((triple7) -> rule2)) -> rule3)) -> rule4))] Gary is round.[(triple6)] Gary is young.[(triple7)] @1: Dave is white.[(((triple2) -> rule2))] Gary is white.[(((triple7) -> rule2))] @2: Dave is quiet.[(((((triple2) -> rule2)) -> rule3))] Gary is quiet.[(((((triple7) -> rule2)) -> rule3))] @3: Dave is green.[(((((((triple2) -> rule2)) -> rule3) triple2) -> rule6))] Dave is rough.[(((((((triple2) -> rule2)) -> rule3)) -> rule4))] Gary is green.[(((((((triple7) -> rule2)) -> rule3) triple7) -> rule6))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is not round.
("Erin" "is" "round" "-")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple7) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3