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