Anne is kind. Anne is round. Anne is young. Bob is smart. Charlie is big. Charlie is nice. Charlie is not young. Gary is big. Gary is smart. Gary is young. All big things are round. If something is round and not young then it is big. All nice things are big. Young things are big. If Gary is nice then Gary is smart. All nice, kind things are rough. If something is smart then it is nice. If Anne is young then Anne is rough. If something is round then it is kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is round and not young then it is big.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Gary is nice then Gary is smart.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
All nice, kind things are rough.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Anne is young then Anne is rough.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "rough" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Charlie is big.
True
1
proof
[(triple5 OR ((triple6) -> rule3))]
("Charlie" "is" "big" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule3))]
("Charlie" "is" "big" "-")
triple5
((triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is nice.
True
2
proof
[(((triple4) -> rule7))]
("Bob" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple3) -> rule4))]
("Anne" "is" "big" "-")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is big.
True
3
proof
[(((((triple4) -> rule7)) -> rule3))]
("Bob" "is" "big" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule9) OR ((((((triple6) -> rule3)) -> rule1)) -> rule9))]
("Charlie" "is" "kind" "-")
((((triple5) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
True
5
proof
[(((triple6 ((((triple5) -> rule1)) -> rule9)) -> rule6) OR ((triple6 ((((((triple6) -> rule3)) -> rule1)) -> rule9)) -> rule6))]
("Charlie" "is" "rough" "+")
((triple6 ((((triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not rough.
False
5
inv-proof
[(((triple6 ((((triple5) -> rule1)) -> rule9)) -> rule6) OR ((triple6 ((((((triple6) -> rule3)) -> rule1)) -> rule9)) -> rule6))]
("Charlie" "is" "rough" "-")
((triple6 ((((triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Bob is kind.
True
5
proof
[(((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9))]
("Bob" "is" "kind" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is not kind.
False
5
inv-proof
[(((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9))]
("Bob" "is" "kind" "-")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is rough.
True
8
proof
[(((((triple4) -> rule7) ((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9)) -> rule6))]
("Bob" "is" "rough" "+")
((((triple4) -> (rule7 % int5)) ((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Bob is not rough.
False
8
inv-proof
[(((((triple4) -> rule7) ((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9)) -> rule6))]
("Bob" "is" "rough" "-")
((((triple4) -> (rule7 % int5)) ((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "nice" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1 OR ((triple2) -> rule9) OR ((((((triple3) -> rule4)) -> rule1)) -> rule9))] Anne is round.[(triple2 OR ((((triple3) -> rule4)) -> rule1))] Anne is young.[(triple3)] Bob is smart.[(triple4)] Charlie is big.[(triple5 OR ((triple6) -> rule3))] Charlie is nice.[(triple6)] Charlie is not young.[(triple7)] Gary is big.[(triple8 OR ((triple10) -> rule4) OR ((((triple9) -> rule7)) -> rule3))] Gary is smart.[(triple9)] Gary is young.[(triple10)] @1: Anne is big.[(((triple3) -> rule4))] Anne is rough.[(((triple3) -> rule8))] Bob is nice.[(((triple4) -> rule7))] Charlie is round.[(((triple5) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] Gary is nice.[(((triple9) -> rule7))] Gary is round.[(((triple8) -> rule1) OR ((((triple10) -> rule4)) -> rule1) OR ((((((triple9) -> rule7)) -> rule3)) -> rule1))] @2: Bob is big.[(((((triple4) -> rule7)) -> rule3))] Charlie is kind.[(((((triple5) -> rule1)) -> rule9) OR ((((((triple6) -> rule3)) -> rule1)) -> rule9))] Gary is kind.[(((((triple8) -> rule1)) -> rule9) OR ((((((triple10) -> rule4)) -> rule1)) -> rule9) OR ((((((((triple9) -> rule7)) -> rule3)) -> rule1)) -> rule9))] @3: Bob is round.[(((((((triple4) -> rule7)) -> rule3)) -> rule1))] Charlie is rough.[(((triple6 ((((triple5) -> rule1)) -> rule9)) -> rule6) OR ((triple6 ((((((triple6) -> rule3)) -> rule1)) -> rule9)) -> rule6))] Gary is rough.[(((((triple9) -> rule7) ((((triple8) -> rule1)) -> rule9)) -> rule6) OR ((((triple9) -> rule7) ((((((triple10) -> rule4)) -> rule1)) -> rule9)) -> rule6) OR ((((triple9) -> rule7) ((((((((triple9) -> rule7)) -> rule3)) -> rule1)) -> rule9)) -> rule6))] @4: Bob is kind.[(((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9))] @5: Bob is rough.[(((((triple4) -> rule7) ((((((((triple4) -> rule7)) -> rule3)) -> rule1)) -> rule9)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple2) -> (rule9 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple10) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple9) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple8) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple5) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((triple8) -> (rule1 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((((triple9) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((((((triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple6 ((((triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
((((triple9) -> (rule7 % int4)) ((((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((triple9) -> (rule7 % int5)) ((((((triple10) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5
((((triple9) -> (rule7 % int5)) ((((((((triple9) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5
Bob is kind.
("Bob" "is" "kind" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
((((triple4) -> (rule7 % int5)) ((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5