Bob is big. Bob is furry. Bob is nice. Fiona is quiet. Fiona is rough. Harry is not big. Harry is nice. If someone is big and not nice then they are furry. Big, kind people are red. If Bob is big and Bob is kind then Bob is furry. If someone is red and kind then they are rough. All quiet, nice people are not rough. Furry people are kind. All furry, nice people are kind. If Harry is big and Harry is rough then Harry is not quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is nice.
("Harry" "is" "nice" "+")
If someone is big and not nice then they are furry.
((("someone" "is" "big" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Big, kind people are red.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Bob is big and Bob is kind then Bob is furry.
((("Bob" "is" "big" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "furry" "+"))
If someone is red and kind then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All quiet, nice people are not rough.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All furry, nice people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Harry is big and Harry is rough then Harry is not quiet.
((("Harry" "is" "big" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "quiet" "-"))
Fiona is quiet.
True
1
proof
[(triple4)]
("Fiona" "is" "quiet" "+")
triple4
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is kind.
True
2
proof
[(((triple2) -> rule6) OR ((triple2 triple3) -> rule7))]
("Bob" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 triple3) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule6) OR ((triple2 triple3) -> rule7))]
("Bob" "is" "kind" "-")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 triple3) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
True
4
proof
[(((triple1 ((triple2) -> rule6)) -> rule2) OR ((triple1 ((triple2 triple3) -> rule7)) -> rule2))]
("Bob" "is" "red" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not red.
False
4
inv-proof
[(((triple1 ((triple2) -> rule6)) -> rule2) OR ((triple1 ((triple2 triple3) -> rule7)) -> rule2))]
("Bob" "is" "red" "-")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
True
7
proof
[(((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4))]
("Bob" "is" "rough" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not rough.
False
7
inv-proof
[(((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4))]
("Bob" "is" "rough" "-")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "+")
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Fiona is quiet.[(triple4)] Fiona is rough.[(triple5)] Harry is nice.[(triple7)] Harry is not big.[(triple6)] @1: Bob is kind.[(((triple2) -> rule6) OR ((triple2 triple3) -> rule7))] @2: Bob is red.[(((triple1 ((triple2) -> rule6)) -> rule2) OR ((triple1 ((triple2 triple3) -> rule7)) -> rule2))] @3: Bob is rough.[(((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2) -> rule6)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2) -> rule6)) -> rule4) OR ((((triple1 ((triple2 triple3) -> rule7)) -> rule2) ((triple2 triple3) -> rule7)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 triple3) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3