Bob is big. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is round. Bob is white. Charlie is big. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is round. Dave is cold. Dave is white. Gary is cold. Gary is quiet. Cold things are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Charlie is cold.
True
1
proof
[(triple9)]
("Charlie" "is" "cold" "+")
triple9
Charlie is not big.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "big" "-")
triple8
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5 OR ((triple2) -> rule1))] Bob is round.[(triple6)] Bob is white.[(triple7)] Charlie is big.[(triple8)] Charlie is cold.[(triple9)] Charlie is furry.[(triple10)] Charlie is nice.[(triple11)] Charlie is round.[(triple12)] Dave is cold.[(triple13)] Dave is white.[(triple14)] Gary is cold.[(triple15)] Gary is quiet.[(triple16 OR ((triple15) -> rule1))] @1: Charlie is quiet.[(((triple9) -> rule1))] Dave is quiet.[(((triple13) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is furry.
("Charlie" "is" "furry" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple14
Gary is cold.
("Gary" "is" "cold" "+")
triple15
Gary is quiet.
("Gary" "is" "quiet" "+")
triple16
((triple15) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple9) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple13) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1