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