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