Bob is big. Bob is not red. Bob is not white. Dave is blue. Dave is red. Dave is round. Erin is blue. Erin is quiet. Erin is red. Erin is white. Red people are blue. All round, blue people are quiet. Quiet people are kind. All quiet, round people are big. If someone is red and not blue then they are round. All kind people are round. If someone is red and not round then they are white. If someone is big and not round then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is not white.
("Bob" "is" "white" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All round, blue people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All quiet, round people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is red and not blue then they are round.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "round" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is red and not round then they are white.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "+"))
If someone is big and not round then they are white.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "+"))
Erin is quiet.
True
1
proof
[(triple8)]
("Erin" "is" "quiet" "+")
triple8
Erin is not blue.
False
1
inv-proof
[(triple7 OR ((triple9) -> rule1))]
("Erin" "is" "blue" "-")
triple7
((triple9) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
True
2
proof
[(((triple8) -> rule3))]
("Erin" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple6 triple4) -> rule2) OR ((triple6 ((triple5) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "-")
((triple6 triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is round.
True
3
proof
[(((((triple8) -> rule3)) -> rule6))]
("Erin" "is" "round" "+")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule6))]
("Erin" "is" "round" "-")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
True
5
proof
[(((triple8 ((((triple8) -> rule3)) -> rule6)) -> rule4))]
("Erin" "is" "big" "+")
((triple8 ((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not big.
False
5
inv-proof
[(((triple8 ((((triple8) -> rule3)) -> rule6)) -> rule4))]
("Erin" "is" "big" "-")
((triple8 ((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is kind.
Unknown
rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not round.
Unknown
inv-rconc
[@4: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is not red.[(triple2)] Bob is not white.[(triple3)] Dave is blue.[(triple4 OR ((triple5) -> rule1))] Dave is red.[(triple5)] Dave is round.[(triple6)] Erin is blue.[(triple7 OR ((triple9) -> rule1))] Erin is quiet.[(triple8)] Erin is red.[(triple9)] Erin is white.[(triple10)] @1: Dave is quiet.[(((triple6 triple4) -> rule2) OR ((triple6 ((triple5) -> rule1)) -> rule2))] Erin is kind.[(((triple8) -> rule3))] @2: Dave is big.[(((((triple6 triple4) -> rule2) triple6) -> rule4) OR ((((triple6 ((triple5) -> rule1)) -> rule2) triple6) -> rule4))] Dave is kind.[(((((triple6 triple4) -> rule2)) -> rule3) OR ((((triple6 ((triple5) -> rule1)) -> rule2)) -> rule3))] Erin is round.[(((((triple8) -> rule3)) -> rule6))] @3: Erin is big.[(((triple8 ((((triple8) -> rule3)) -> rule6)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
((triple9) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6 triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple6 triple4) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple6 ((triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple6 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple6 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple8 ((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3