Bob is big. Bob is cold. Bob is nice. Bob is quiet. Dave is big. Dave is cold. Dave is nice. Dave is quiet. Dave is round. Dave is white. If something is big then it is white. If Dave is white and Dave is quiet then Dave is cold. If Dave is blue then Dave is quiet. If Dave is blue and Dave is quiet then Dave is cold. If Bob is big and Bob is blue then Bob is round. All blue things are nice. If something is quiet and round then it is big. Blue things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Dave is white and Dave is quiet then Dave is cold.
((("Dave" "is" "white" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
If Dave is blue then Dave is quiet.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "quiet" "+"))
If Dave is blue and Dave is quiet then Dave is cold.
((("Dave" "is" "blue" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
If Bob is big and Bob is blue then Bob is round.
((("Bob" "is" "big" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and round then it is big.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Dave is nice.
True
1
proof
[(triple7)]
("Dave" "is" "nice" "+")
triple7
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Dave is big.[(triple5 OR ((triple8 triple9) -> rule7))] Dave is cold.[(triple6 OR ((triple10 triple8) -> rule2) OR ((((triple5) -> rule1) triple8) -> rule2) OR ((((((triple8 triple9) -> rule7)) -> rule1) triple8) -> rule2))] Dave is nice.[(triple7)] Dave is quiet.[(triple8)] Dave is round.[(triple9)] Dave is white.[(triple10 OR ((triple5) -> rule1) OR ((((triple8 triple9) -> rule7)) -> rule1))] @1: Bob is white.[(((triple1) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple8 triple9) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((triple10 triple8) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple5) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple8 triple9) -> (rule7 % int3))) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple5) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple8 triple9) -> (rule7 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1