Bob is big. Bob is furry. Bob is not green. Bob is rough. Dave is blue. Dave is quiet. Dave is red. Dave is rough. Fiona is not big. Fiona is green. Fiona is rough. Gary is big. Gary is quiet. Gary is red. Gary is rough. If someone is quiet and not big then they are rough. All big people are rough. Green, furry people are quiet. If someone is blue and not big then they are red. All rough people are red. If Bob is rough and Bob is not furry then Bob is not green.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is quiet and not big then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Green, furry people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and not big then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "+"))
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Bob is rough and Bob is not furry then Bob is not green.
((("Bob" "is" "rough" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "green" "-"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Fiona is big.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "big" "+")
triple9
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is not green.[(triple3)] Bob is rough.[(triple4 OR ((triple1) -> rule2))] Dave is blue.[(triple5)] Dave is quiet.[(triple6)] Dave is red.[(triple7 OR ((triple8) -> rule5))] Dave is rough.[(triple8)] Fiona is green.[(triple10)] Fiona is not big.[(triple9)] Fiona is rough.[(triple11)] Gary is big.[(triple12)] Gary is quiet.[(triple13)] Gary is red.[(triple14 OR ((triple15) -> rule5) OR ((((triple12) -> rule2)) -> rule5))] Gary is rough.[(triple15 OR ((triple12) -> rule2))] @1: Bob is red.[(((triple4) -> rule5) OR ((((triple1) -> rule2)) -> rule5))] Fiona is red.[(((triple11) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not green.
("Bob" "is" "green" "-")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple8) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is not big.
("Fiona" "is" "big" "-")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple15) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((triple11) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1