Bob is furry. Bob is round. Bob is smart. Bob is white. Dave is kind. Dave is quiet. Dave is round. Erin is big. Erin is kind. Erin is round. Erin is smart. Harry is smart. All kind, quiet things are smart. If something is smart then it is white. All kind things are big. Furry, white things are smart. If something is smart then it is quiet. If Dave is big then Dave is kind.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All kind, quiet things are smart.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Dave is big then Dave is kind.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
Erin is smart.
True
1
proof
[(triple11)]
("Erin" "is" "smart" "+")
triple11
Bob is not white.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule2))]
("Bob" "is" "white" "-")
triple4
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is smart.
True
3
proof
[(((triple5 triple6) -> rule1))]
("Dave" "is" "smart" "+")
((triple5 triple6) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule5) OR ((((triple1 triple4) -> rule4)) -> rule5))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is white.
True
4
proof
[(((((triple5 triple6) -> rule1)) -> rule2))]
("Dave" "is" "white" "+")
((((triple5 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not white.
False
4
inv-proof
[(((((triple5 triple6) -> rule1)) -> rule2))]
("Dave" "is" "white" "-")
((((triple5 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3 OR ((triple1 triple4) -> rule4))] Bob is white.[(triple4 OR ((triple3) -> rule2))] Dave is kind.[(triple5)] Dave is quiet.[(triple6)] Dave is round.[(triple7)] Erin is big.[(triple8 OR ((triple9) -> rule3))] Erin is kind.[(triple9)] Erin is round.[(triple10)] Erin is smart.[(triple11)] Harry is smart.[(triple12)] @1: Bob is quiet.[(((triple3) -> rule5) OR ((((triple1 triple4) -> rule4)) -> rule5))] Dave is big.[(((triple5) -> rule3))] Dave is smart.[(((triple5 triple6) -> rule1))] Erin is quiet.[(((triple11) -> rule5))] Erin is white.[(((triple11) -> rule2))] Harry is quiet.[(((triple12) -> rule5))] Harry is white.[(((triple12) -> rule2))] @2: Dave is white.[(((((triple5 triple6) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple1 triple4) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple9) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5 triple6) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple11) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple11) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple12) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple5 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2