Bob is big. Bob is not cold. Bob is kind. Bob is quiet. Bob is round. Charlie is smart. Dave is not big. Dave is not cold. Dave is not quiet. Dave is round. If Bob is big and Bob is kind then Bob is round. Cold, round people are not furry. If Dave is kind then Dave is furry. All round people are smart. All furry, kind people are smart. All cold people are round. Kind people are quiet. If Dave is cold and Dave is not round then Dave is quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is round.
("Dave" "is" "round" "+")
If Bob is big and Bob is kind then Bob is round.
((("Bob" "is" "big" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "round" "+"))
Cold, round people are not furry.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "-"))
If Dave is kind then Dave is furry.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "furry" "+"))
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All furry, kind people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is cold and Dave is not round then Dave is quiet.
((("Dave" "is" "cold" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "quiet" "+"))
Bob is round.
True
1
proof
[(triple5 OR ((triple1 triple3) -> rule1))]
("Bob" "is" "round" "+")
triple5
((triple1 triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple10)]
("Dave" "is" "round" "-")
triple10
Bob is smart.
True
2
proof
[(((triple5) -> rule4) OR ((((triple1 triple3) -> rule1)) -> rule4))]
("Bob" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not smart.
False
2
inv-proof
[(((triple5) -> rule4) OR ((((triple1 triple3) -> rule1)) -> rule4))]
("Bob" "is" "smart" "-")
((triple5) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple3)] Bob is not cold.[(triple2)] Bob is quiet.[(triple4 OR ((triple3) -> rule7))] Bob is round.[(triple5 OR ((triple1 triple3) -> rule1))] Charlie is smart.[(triple6)] Dave is not big.[(triple7)] Dave is not cold.[(triple8)] Dave is not quiet.[(triple9)] Dave is round.[(triple10)] @1: Bob is smart.[(((triple5) -> rule4) OR ((((triple1 triple3) -> rule1)) -> rule4))] Dave is smart.[(((triple10) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple1 triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Dave is not big.
("Dave" "is" "big" "-")
triple7
Dave is not cold.
("Dave" "is" "cold" "-")
triple8
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple10) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1