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