Anne is big. Anne is green. Anne is round. Anne is white. Bob is big. Bob is furry. Bob is nice. Bob is white. Dave is furry. Dave is green. Dave is round. Dave is white. Erin is big. Erin is smart. Erin is white. All round things are big. Furry, white things are round. All green, nice things are round. White, round things are smart. All smart, round things are white. Smart things are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Furry, white things are round.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All green, nice things are round.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
White, round things are smart.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All smart, round things are white.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Dave is round.
True
1
proof
[(triple11 OR ((triple9 triple12) -> rule2))]
("Dave" "is" "round" "+")
triple11
((triple9 triple12) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple6)]
("Bob" "is" "furry" "-")
triple6
Erin is green.
True
2
proof
[(((triple14) -> rule6))]
("Erin" "is" "green" "+")
((triple14) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is not smart.
False
3
inv-proof
[(((triple4 triple3) -> rule4))]
("Anne" "is" "smart" "-")
((triple4 triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is smart.
True
5
proof
[(((triple8 ((triple6 triple8) -> rule2)) -> rule4))]
("Bob" "is" "smart" "+")
((triple8 ((triple6 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not smart.
False
5
inv-proof
[(((triple8 ((triple6 triple8) -> rule2)) -> rule4))]
("Bob" "is" "smart" "-")
((triple8 ((triple6 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
True
6
proof
[(((((triple8 ((triple6 triple8) -> rule2)) -> rule4)) -> rule6))]
("Bob" "is" "green" "+")
((((triple8 ((triple6 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not green.
False
6
inv-proof
[(((((triple8 ((triple6 triple8) -> rule2)) -> rule4)) -> rule6))]
("Bob" "is" "green" "-")
((((triple8 ((triple6 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule1))] Anne is green.[(triple2 OR ((((triple4 triple3) -> rule4)) -> rule6))] Anne is round.[(triple3)] Anne is white.[(triple4)] Bob is big.[(triple5 OR ((((triple6 triple8) -> rule2)) -> rule1))] Bob is furry.[(triple6)] Bob is nice.[(triple7)] Bob is white.[(triple8)] Dave is furry.[(triple9)] Dave is green.[(triple10 OR ((((triple12 triple11) -> rule4)) -> rule6) OR ((((triple12 ((triple9 triple12) -> rule2)) -> rule4)) -> rule6))] Dave is round.[(triple11 OR ((triple9 triple12) -> rule2))] Dave is white.[(triple12)] Erin is big.[(triple13)] Erin is smart.[(triple14)] Erin is white.[(triple15)] @1: Anne is smart.[(((triple4 triple3) -> rule4))] Bob is round.[(((triple6 triple8) -> rule2))] Dave is big.[(((triple11) -> rule1) OR ((((triple9 triple12) -> rule2)) -> rule1))] Dave is smart.[(((triple12 triple11) -> rule4) OR ((triple12 ((triple9 triple12) -> rule2)) -> rule4))] Erin is green.[(((triple14) -> rule6))] @2: Bob is smart.[(((triple8 ((triple6 triple8) -> rule2)) -> rule4))] @3: Bob is green.[(((((triple8 ((triple6 triple8) -> rule2)) -> rule4)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
((((triple4 triple3) -> (rule4 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
((((triple6 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
((((triple12 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple12 ((triple9 triple12) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple9 triple12) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple12
Erin is big.
("Erin" "is" "big" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14
Erin is white.
("Erin" "is" "white" "+")
triple15
Anne is smart.
("Anne" "is" "smart" "+")
((triple4 triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple6 triple8) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple12 triple11) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple12 ((triple9 triple12) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple14) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple8 ((triple6 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple8 ((triple6 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3