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