Bob is big. Bob is cold. Dave is big. Dave is furry. Erin is big. Erin is cold. Erin is furry. Erin is kind. Erin is rough. Gary is cold. Gary is round. If Dave is cold then Dave is round. If Gary is rough and Gary is cold then Gary is kind. Quiet people are round. Round, quiet people are kind. If someone is furry then they are rough. If Bob is cold then Bob is quiet. Rough people are quiet. If someone is kind then they are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
If Dave is cold then Dave is round.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "round" "+"))
If Gary is rough and Gary is cold then Gary is kind.
((("Gary" "is" "rough" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "kind" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Round, quiet people are kind.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Bob is cold then Bob is quiet.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "quiet" "+"))
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple3)]
("Dave" "is" "big" "-")
triple3
Dave is rough.
True
2
proof
[(((triple4) -> rule5))]
("Dave" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple4) -> rule5)) -> rule7))]
("Dave" "is" "quiet" "+")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule3) OR ((((((triple7) -> rule5)) -> rule7)) -> rule3))]
("Erin" "is" "round" "-")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Bob is kind.
True
6
proof
[(((((((triple2) -> rule6)) -> rule3) ((triple2) -> rule6)) -> rule4))]
("Bob" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is not round.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule7)) -> rule3))]
("Dave" "is" "round" "-")
((((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
True
8
proof
[(((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4))]
("Dave" "is" "kind" "+")
((((((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is not kind.
False
8
inv-proof
[(((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4))]
("Dave" "is" "kind" "-")
((((((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is cold.
True
9
proof
[(((((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4)) -> rule8))]
("Dave" "is" "cold" "+")
((((((((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule3 % int3)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Dave is not cold.
False
9
inv-proof
[(((((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4)) -> rule8))]
("Dave" "is" "cold" "-")
((((((((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule3 % int3)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is kind.
Unknown
rconc
[@3: Gary is kind.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule5 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Dave is big.[(triple3)] Dave is furry.[(triple4)] Erin is big.[(triple5)] Erin is cold.[(triple6 OR ((triple8) -> rule8) OR ((((((((triple9) -> rule7)) -> rule3) ((triple9) -> rule7)) -> rule4)) -> rule8) OR ((((((((triple9) -> rule7)) -> rule3) ((((triple7) -> rule5)) -> rule7)) -> rule4)) -> rule8) OR ((((((((((triple7) -> rule5)) -> rule7)) -> rule3) ((triple9) -> rule7)) -> rule4)) -> rule8) OR ((((((((((triple7) -> rule5)) -> rule7)) -> rule3) ((((triple7) -> rule5)) -> rule7)) -> rule4)) -> rule8))] Erin is furry.[(triple7)] Erin is kind.[(triple8 OR ((((((triple9) -> rule7)) -> rule3) ((triple9) -> rule7)) -> rule4) OR ((((((triple9) -> rule7)) -> rule3) ((((triple7) -> rule5)) -> rule7)) -> rule4) OR ((((((((triple7) -> rule5)) -> rule7)) -> rule3) ((triple9) -> rule7)) -> rule4) OR ((((((((triple7) -> rule5)) -> rule7)) -> rule3) ((((triple7) -> rule5)) -> rule7)) -> rule4))] Erin is rough.[(triple9 OR ((triple7) -> rule5))] Gary is cold.[(triple10)] Gary is round.[(triple11)] @1: Bob is quiet.[(((triple2) -> rule6))] Dave is rough.[(((triple4) -> rule5))] Erin is quiet.[(((triple9) -> rule7) OR ((((triple7) -> rule5)) -> rule7))] @2: Bob is round.[(((((triple2) -> rule6)) -> rule3))] Dave is quiet.[(((((triple4) -> rule5)) -> rule7))] Erin is round.[(((((triple9) -> rule7)) -> rule3) OR ((((((triple7) -> rule5)) -> rule7)) -> rule3))] @3: Bob is kind.[(((((((triple2) -> rule6)) -> rule3) ((triple2) -> rule6)) -> rule4))] Dave is round.[(((((((triple4) -> rule5)) -> rule7)) -> rule3))] @4: Dave is kind.[(((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4))] @5: Dave is cold.[(((((((((((triple4) -> rule5)) -> rule7)) -> rule3) ((((triple4) -> rule5)) -> rule7)) -> rule4)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple8) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((((((triple9) -> (rule7 % int4))) -> (rule3 % int3)) ((triple9) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple9) -> (rule7 % int5))) -> (rule3 % int4)) ((((triple7) -> (rule5 % int3))) -> (rule7 % int5))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
((((((((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule3 % int3)) ((triple9) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
((((((((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule3 % int3)) ((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((((((triple9) -> (rule7 % int3))) -> (rule3 % int2)) ((triple9) -> (rule7 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple9) -> (rule7 % int4))) -> (rule3 % int3)) ((((triple7) -> (rule5 % int2))) -> (rule7 % int4))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) ((triple9) -> (rule7 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple7) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple9) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
((((((((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule3 % int3)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5