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