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