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