Bob is big. Bob is blue. Bob is smart. Charlie is big. Charlie is green. Charlie is red. Charlie is smart. Dave is blue. Dave is green. Dave is quiet. Dave is red. Dave is not rough. Dave is smart. Gary is quiet. Gary is smart. Rough things are not green. If Dave is blue and Dave is green then Dave is smart. Smart, rough things are quiet. If something is green and not quiet then it is red. Smart things are big. If something is quiet and red then it is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Rough things are not green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "-"))
If Dave is blue and Dave is green then Dave is smart.
((("Dave" "is" "blue" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "smart" "+"))
Smart, rough things are quiet.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is green and not quiet then it is red.
((("something" "is" "green" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is quiet and red then it is big.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1 OR ((triple3) -> rule5))]
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is not green.
False
1
inv-proof
[(triple9)]
("Dave" "is" "green" "-")
triple9
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is big.[(triple1 OR ((triple3) -> rule5))] Bob is blue.[(triple2)] Bob is smart.[(triple3)] Charlie is big.[(triple4 OR ((triple7) -> rule5))] Charlie is green.[(triple5)] Charlie is red.[(triple6)] Charlie is smart.[(triple7)] Dave is blue.[(triple8)] Dave is green.[(triple9)] Dave is not rough.[(triple12)] Dave is quiet.[(triple10)] Dave is red.[(triple11)] Dave is smart.[(triple13 OR ((triple8 triple9) -> rule2))] Gary is quiet.[(triple14)] Gary is smart.[(triple15)] @1: Dave is big.[(((triple13) -> rule5) OR ((triple10 triple11) -> rule6) OR ((((triple8 triple9) -> rule2)) -> rule5))] Gary is big.[(((triple15) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple7) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is not rough.
("Dave" "is" "rough" "-")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple13
((triple8 triple9) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Dave is big.
("Dave" "is" "big" "+")
((triple13) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple10 triple11) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple8 triple9) -> (rule2 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple15) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1