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